Formal specification and verification of complex systems
Gnesi S.
Computer Science(all) Theoretical Computer Science General Computer Science Software verification Program verification
The application of formal methods in the rigorous de nition and analysis of the functionality and the behaviour of a system, promises the ability of showing that the system is correct. Given such a promise, that is already out since several years, it is astonishing to see how little formal methods are actually used in the safety critical system industry, though the use of formal methods is increasingly required by the international standards and guidelines for the development of complex systems.
Source: Electronic notes in theoretical computer science 80 (2003): 1–5. doi:10.1016/S1571-0661(04)80829-6
Publisher: Elsevier, Amsterdam , Paesi Bassi
[9] S. Gnesi, D. Latella, and M. Massink. Model checking UML statechart diagrams using JACK. In A. Williams, editor, Fourth IEEE International High-Assurance Systems Engineering Symposium, pages 46-55. IEEE Computer Society Press, 1999.
[10] S. Gnesi, G. Ristori. A Model Checking Algorithm for π-calculus agents. In Advances in Temporal Logic. Kluwer Academic Publishers, pp.339 - 357, 2000.
[11] S. Gnesi, D. Latella, and G. Lenzini. A BRUTUS logic for the Spi-Calculus. In Proc. of the ACM SIGPLAN and IFIP WG1.7 Worshop on Issues in Theory of Security (WITS 02), 2002.
[12] S. Gnesi, D. Latella, and G. Lenzini. Towards a model checking spi-calculus dialect. Technical Report 0000, Istituto di Elaborazione dell'Informazione - CNR, Pisa, July 2002.
[13] J.C. Laprie (Ed.). Dependability: Basic Concepts and Terminology. Dependable Computing and Fault-Tolerant Systems, vol. 5, Springer-Verlag, 1992.
[14] D. Latella, I. Majzik, and M. Massink. Towards a formal operational semantics of UML statechart diagrams. IFIP TC6/WG6.1 Third International Conference on Formal Methods for Open Object-Oriented Distributed Systems, Kluwer Academic Publishers, 1999.
[15] D. Latella, I. Majzik, and M. Massink. Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker. Formal Aspects of Computing. Springer-Verlag, 2000.
[16] R. Milner. Communication and Concurrency. Prentice-Hall, 1989.
[17] R. Milner, J. Parrow and D. Walker. A calculus of mobile processes (parts I and II). Information and Computation, 100:1-77, 1992.
[18] U. Montanari and M. Pistore. Checking bisimilarity for finitary π-calculus. In Proc. CONCUR'95, LNCS 962. Springer Verlag, 1995.
[19] D. Powell, et al. GUARDS: a Generic Upgradable Architecture for Real-time Dependable Systems. IEEE Transactions on Computers, 1999.
[20] J. Rumbaugh, I. Jacobson, and G. Booch. The Unified Modeling Language Reference Manual. Addison-Wesley, 1999.
Metrics
Back to previous page
@article{oai:it.cnr:prodotti:68423,
title = {Formal specification and verification of complex systems},
author = {Gnesi S.},
publisher = {Elsevier, Amsterdam , Paesi Bassi},
doi = {10.1016/s1571-0661(04)80829-6},
journal = {Electronic notes in theoretical computer science},
volume = {80},
pages = {1–5},
year = {2003}
}
0000-0002-0139-0421