Deductive verification of requirements for event-driven architecture

A.A. Letichevsky, O.O. Letichevsky, V.S. Peschanenko, A.A. Guba

Abstract


The current paper presents the technology of processing of requirements for systems with event-driven architecture. The technology consists of the stages of formalization, formal verification and conversion to design specifications. The formalization is the formal description of events as formal specifications called basic protocols. The consistency and completeness of basic protocols, safety properties and user-defined properties are verified. The deductive tools for dynamic and static checking are used for detection of properties violation. The method of enlargement allows reducing the complexity of proving and solving. Formal presentation of requirements allows converting them to SDL\UML specifications and generating the test suite. The technology is realized in IMS system and applied in more than 50 projects of telecommunication, networking, microprocessing and automotive systems.

Problems in programming 2013; 2: 54-61


Full Text:

PDF

References


Holzmann G.J. The Spin Model Checker, Primer and Reference Manual. Addison Wesley, 2003, 596 p.

Holzmann G. "The Model Checker SPIN" // IEEE Trans. on Software Engineering. – Vol. 23, № 5, – 1997. – P. 279–295.

International Telecommunications Union.Recommendation Z.151 – User Requirements Notation (URN). – 2008.

Gunter Mussbacher. Aspect-Oriented User Requirements Notation. Thesis submitted to the Faculty of Graduate and Postdoctoral Studies in partial fulfillment of the requirements for the degree of Ph.D. in Computer Science. University of Ottawa, Ottawa, Canada, September 2010.

David Aspinall. Proof general: A generic tool for proof development. In Susanne Graf and Michael I. Schwartzbach, editors, TACAS,

volume 1785 of Lecture Notes in Computer Science, pages 38–42. Springer, 2000.

Autexier S., Hutter D., Mantel H., and Schairer A. Towards an evolutionary formal software-development using Casl. In C.

Choppy and D. Bert, editors, Recent Trends in Algebraic Development Techniques // 14th International Workshop, WADT’99, Bonas,

France, Vol. 1827 of Lecture Notes in Computer Science. – Springer-Verlag, 2000. P. 73–88.

Nikolaj Bjørner, Anca Browne, Eddie Chang, Michael Colón, Arjun Kapur, Zohar Manna, Henny B. Sipma and Tomás E. Uribe. STeP:

Deductive-Algorithmic Verification of Reactive and Real-time Systems.

Sam Owre, John Rushby, N. Shankar and David Stringer-Calvert. PVS: An Experience Report. Applied Formal Methods, FM-Trends

, Boppard, Germany, October 1998.

Information Technology — Z Formal Specification Notation — Syntax, Type System and Semantics (ISO/IEC 13568:2002 ed.). 2002

-01. P. 196.

Spivey J.M. The Z Notation: A Reference Manual. Prentice-Hall International, New Jersey, second edition, 1992.

Brucker A.D., Rittinger F., and Wolff B. HOL-Z 2.0: A proof environment for Zspecifications. Journal of Universal Computer Science. – Feb. 2003. – 9(2). – P. 152–172.

Nipkow T., Paulson L.C., and Wenzel M. Isabelle/HOL — A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002.

Letichevsky A., Kapitonova J., Letichevsky A. jr., Volkov V., Baranov S., Kotlyarov V., Weigert T. Basic Protocols, Message Sequence Charts, and the Verification of Requirements Specifications // Computer Networks. – 2005. – Vol. 47. – P. 662–675.

Letichevsky A., Kapitonova J., Volkov V., Letichevsky A. jr., Baranov S., Kotlyarov V., and Weigert T. System Specification with Basic

Protocols // Cybernetics and System Analyses. – 2005. – Vol. 4. – P. 3–21.

Letichevsky A.A., Godlevsky A.B., Letichevsky A.A. Jr., Potienko S.V., Peschanenko V.S. Properties of Predicate Transformer of VRS

System // Cybernetics and System Analyses. – 2010. – Vol. 4. – p. 3–16.

International Telecommunications Union. Recommendation Z. 120 – Message Sequence Chart (MSC), 84 p.

Symbolic modeling, http://en.wikipedia.org/wiki/Model_checking

Letichevsky A., Letychevskyi O., Peschanenko V. Insertion Modeling System. In: Clarke E.M., Virbitskaite I., Voronkov A. (eds.) PSI

LNCS, Vol. 7162, P. 262–274. Springer, Heidelberg (2011)

APS&IMS Systems, http://apsystem.org.ua


Refbacks

  • There are currently no refbacks.