Abstract
The motivation for this study comes from various sources such as parametric formal verification, requirements engineering, and safety analysis. In these areas, there are often situations in which we are given a set of configurations and a property of interest with the goal of computing all the configurations for which the property is valid. Checking the validity of each single configuration may be a costly process. We are thus interested in reducing the number of such validity queries. In this work, we assume that the configuration space is equipped with a partial ordering that is preserved by the property to be checked. In such a case, the set of all valid configurations can be effectively represented by the set of all maximum valid (or minimum invalid) configurations w.r.t. the ordering. We show an algorithm to compute such boundary elements. We explain how this general setting applies to consistency and redundancy checking of requirements and to finding minimum cut-sets for safety analysis. We further discuss various heuristics and evaluate their efficiency, measured primarily by the number of validity queries, on a preliminary set of experiments.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Bailey, J., Stuckey, P.J.: Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization. In: Hermenegildo, M.V., Cabeza, D. (eds.) PADL 2004. LNCS, vol. 3350, pp. 174–186. Springer, Heidelberg (2005)
Barnat, J., Bauch, P., Beneš, N., Brim, L., Beran, J., Kratochvíla, T.: Analysing sanity of requirements for avionics systems. Form. Aspects Comput. 28(1), 45–63 (2016). doi:10.1007/s00165-015-0348-9
Barnat, J., Bauch, P., Brim, L.: Checking sanity of software requirements. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 48–62. Springer, Heidelberg (2012)
Barnat, J., Brim, L., Krejci, A., Streck, A., Safranek, D., Vejnar, M., Vejpustek, T.: On parameter synthesis by parallel model checking. IEEE/ACM Trans. Comput. Biol. Bioinform. 9(3), 693–705 (2012)
Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in temporal model checking. Form. Methods Syst. Des. 18(2), 141–163 (2001)
Belov, A., Marques-Silva, J.: MUSer2: an efficient MUS extractor. J. Satisfiability Boolean Model. Comput. 8, 123–128 (2012)
Chen, Y., Chen, Y.: On the decomposition of posets. In: 2012 International Conference on Computer Science Service System (CSSS), pp. 134–138 (2012)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Dajani-Brown, S., Cofer, D., Hartmann, A.C., Pratt, T.W.: Formal modeling and analysis of an avionics triplex sensor voter. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 34–48. Springer, Heidelberg (2003)
Dilworth, R.P.: A decomposition theorem for partially ordered sets. Ann. Math. 51(1), 161–166 (1950)
Fulkerson, D.R.: Note on Dilworth’s decomposition theorem for partially ordered sets. Proc. Am. Math. Soc. 7(4), 701–702 (1956)
Hinchey, M., Jackson, M., Cousot, P., Cook, B., Bowen, J.P., Margaria, T.: Software engineering and formal methods. Commun. ACM 51, 54–59 (2008)
Joshi, A., Miller, S.P., Whalen, M., Heimdahl, M.P.: A proposal for model-based safety analysis. In: The 24th Digital Avionics Systems Conference, 2005. DASC 2005, vol. 2. IEEE (2005)
Lauria, M.: CNFgen formula generator. http://massimolauria.github.io/cnfgen/. Accessed 11 Jan 2016
Liffiton, M.H., Previti, A., Malik, A., Marques-Silva, J.: Fast, flexible MUS enumeration. Constraints 21(2), 223–250 (2016). http://link.springer.com/article/10.1007%2Fs10601-015-9183-0
Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reason. 40(1), 1–33 (2008)
Acknowledgement
The research leading to these results has received funding from the European Unions Seventh Framework Program (FP7/2007-2013) for CRYSTAL Critical System Engineering Acceleration Joint Undertaking under grant agreement No. 332830 and from specific national programs and/or funding authorities.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Bendík, J., Beneš, N., Barnat, J., Černá, I. (2016). Finding Boundary Elements in Ordered Sets with Application to Safety and Requirements Analysis. In: De Nicola, R., Kühn, E. (eds) Software Engineering and Formal Methods. SEFM 2016. Lecture Notes in Computer Science(), vol 9763. Springer, Cham. https://doi.org/10.1007/978-3-319-41591-8_9
Download citation
DOI: https://doi.org/10.1007/978-3-319-41591-8_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-41590-1
Online ISBN: 978-3-319-41591-8
eBook Packages: Computer ScienceComputer Science (R0)