zbMATH — the first resource for mathematics

An abstract interpretation-based model for safety semantics. (English) Zbl 1215.68125
Summary: We describe safety semantics as abstract interpretation of a trace-based operational semantics of a transition system. Intuitively, a property is safety if ‘nothing bad will happen’. Formally this is described by saying that a property is safety if it is maximal with respect to a given set of allowed partial executions. We show that this can be specified in the standard Cousot’s framework of abstract interpretation. In particular, we show that this semantics can be derived as fixpoint of a semantic operator. This construction provides a formal characterization of the constructive nature of safety properties that can be enforced by means of execution monitors. By using the same construction, we show that while safety without stuttering preserves the constructive nature, safety properties allowing cancellation of states lose the constructive characterization. Finally, we characterize safety properties as the closed elements of a closure, and we show that in the abstract interpretation framework safety and liveness properties lose their complementary nature.

68Q55 Semantics in the theory of computing
68Q60 Specification and verification (program logics, model checking, etc.)
68Q70 Algebraic theory of languages and automata
Full Text: DOI
[1] Abramsky S., Handbook of Logic in Computer Science 3 pp 1– (1994) · Zbl 0829.68111
[2] DOI: 10.1016/0020-0190(85)90056-0 · Zbl 0575.68030 · doi:10.1016/0020-0190(85)90056-0
[3] DOI: 10.1007/BF01782772 · Zbl 0641.68039 · doi:10.1007/BF01782772
[4] DOI: 10.1016/0020-0190(86)90132-8 · Zbl 0619.68019 · doi:10.1016/0020-0190(86)90132-8
[5] DOI: 10.1145/6490.6494 · Zbl 0627.68015 · doi:10.1145/6490.6494
[6] Baier C., Fund. Inform. 41 pp 259– (2000)
[7] Birkhoff G., Lattice Theory, 3. ed. (1967)
[8] Chang, E., Manna, Z. and Pnueli, A. Characterization of temporal property classes. Proceedings of the International Colloquium on Automata, Languages and Programming (ICALP ’92). Edited by: Kuich, W. Vol. 623, pp.474–486. Berlin: Springer-Verlag. Lecture Notes in Computer Science
[9] DOI: 10.1145/239912.239914 · Zbl 01936068 · doi:10.1145/239912.239914
[10] DOI: 10.1016/S0304-3975(00)00313-3 · Zbl 0996.68119 · doi:10.1016/S0304-3975(00)00313-3
[11] Cousot, P. and Cousot, R. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. Proceedings of Conference Record of the 4th ACM Symposium on Principles of Programming Languages (POPL ’77). pp.238–252. New York: ACM Press. · Zbl 1149.68389
[12] Cousot P., Pacific J. Math. 82 pp 43– (1979) · Zbl 0413.06004 · doi:10.2140/pjm.1979.82.43
[13] Cousot, P. and Cousot, R. Systematic design of program analysis frameworks. Proceedings of Conference Record of the 6th ACM Symposium on Principles of Programming Languages (POPL ’79). pp.269–282. New York: ACM Press. · Zbl 1323.68356
[14] Cousot, P. and Cousot, R. Inductive definitions, semantics and abstract interpretation. Proceedings of Conference Record of the 19th ACM Symposium on Principles of Programming Languages (POPL ’92). pp.83–94. New York: ACM Press. · Zbl 1248.68316
[15] de Bakker J., Mathematical Theory of Program Correctness (1980)
[16] DOI: 10.1145/360933.360975 · Zbl 0308.68017 · doi:10.1145/360933.360975
[17] Dijkstra E. W., A Discipline of Programming (1976) · Zbl 0368.68005
[18] Dwinger P., Indag. Math. 16 pp 560– (1954) · doi:10.1016/S1385-7258(54)50072-7
[19] FilĂ©, G. and Ranzato, F. Complementation of abstract domains made easy. Proceedings of the 1996 Joint International Conference and Symposium on Logic Programming (JICSLP ’96). Edited by: Maher, M. J. pp.348–362. Cambridge, MA: The MIT Press.
[20] Fong, P. W. Access control by tracking shallow execution history. Proceedings of the 2004 IEEE Symposium on Security and Privacy. pp.43–55. Washington, DC: IEEE Computer Society.
[21] Giacobazzi, R. and Ranzato, F. Refining and compressing abstract domains. Proceedings of the 24th International Colloquium on Automata, Languages and Programming (ICALP ’97). Edited by: Goos, G., Hartmanis, J. and van Leeuwen, J. Vol. 1256, pp.771–781. Berlin: Springer-Verlag. Lecture Notes in Computer Science · Zbl 1401.68197
[22] DOI: 10.1007/BF01236765 · Zbl 0901.06003 · doi:10.1007/BF01236765
[23] DOI: 10.1145/333979.333989 · Zbl 1133.68370 · doi:10.1145/333979.333989
[24] Gierz G., A Compendium of Continuous Lattices (1980) · Zbl 0452.06001 · doi:10.1007/978-3-642-67678-9
[25] DOI: 10.1016/0020-0190(93)90074-J · Zbl 0788.68046 · doi:10.1016/0020-0190(93)90074-J
[26] DOI: 10.1145/1111596.1111601 · Zbl 05459275 · doi:10.1145/1111596.1111601
[27] DOI: 10.1145/363235.363259 · Zbl 0179.23105 · doi:10.1145/363235.363259
[28] DOI: 10.1109/TSE.1977.229904 · Zbl 0349.68006 · doi:10.1109/TSE.1977.229904
[29] DOI: 10.1145/177492.177726 · doi:10.1145/177492.177726
[30] Ligatti, J., Bauer, L. and Walker, D. Enforcing non-safety security policies with program monitors. 10th European Symposium on Research in Computer Security (ESORICS). Edited by: di Vimercati, S. D.C., Syverson, P. F. and Gollmann, D. Vol. 3679, pp.355–373. Berlin: Springer-Verlag. Lecture Notes in Computer Science
[31] Morgado J., Port. Math. 21 pp 135– (1962)
[32] DOI: 10.1145/357172.357178 · Zbl 0483.68013 · doi:10.1145/357172.357178
[33] Paun, D. O. April 1999. ”Closure under stuttering in temporal formulas”. April, Toronto, Ontario: Dept. of Computer Science, University of Toronto. Master’s thesis
[34] Plotkin G., A Structural Approach to Operational Semantics (1981)
[35] DOI: 10.1145/353323.353382 · Zbl 01935075 · doi:10.1145/353323.353382
[36] Shmuely Z., Pacific J. Math. 54 pp 209– (1974) · doi:10.2140/pjm.1974.54.209
[37] DOI: 10.1007/BF01211865 · Zbl 0820.68077 · doi:10.1007/BF01211865
[38] Sistla, A. P. On characterization of safety and liveness properties in temporal logic. Proceedings of the 4th ACM Symposium on Principles of Distributed Computing. Edited by: Malcolm, M. and Strong, R. New York: ACM Press. · Zbl 0820.68077
[39] Smyth M. B., Handbook of Logic in Computer Science (Vol. 1): Background: Mathematical Structures 1 pp 641– (1992)
[40] Thomas W., Schriften Zur Informatik, Bericht 116 (1986)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.