×

Systems specification by basic protocols. (English. Russian original) Zbl 1103.68370

Cybern. Syst. Anal. 41, No. 4, 479-493 (2005); translation from Kibern. Sist. Anal. 2005, No. 4, 3-21 (2005).
Summary: Theoretical foundations of requirements formalization and verification based on basic protocols are presented. This approach uses the concept of an attributed transition system. Facets of an implementation of the system VRS are described together with some statistical results of using this tool in large-scale industrial projects.

MSC:

68M12 Network protocols

Software:

ACL2; APS-1; APS
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] J. Brackett, ”Software Requirements,” Techn. Rep. SEI-CM-19-1.2, Software Eng. Ins. (1990).
[2] S. Owre, N. Shankar, and J. M. Rushby, ”User guide for the PVS specification and verification system,” Techn. Rep., SRI International (1996).
[3] ITU-T. Recommendation Z. 120: Message Sequence Charts (MSCs), ITU-T, Geneva (1999).
[4] ITU-T. Recommendation Z. 100: Specification and Description Language (SDL), ITU-T, Geneva (1999).
[5] OMG. Unified Modeling Language Specification, 2.0, OMG, Needham (2003).
[6] P. Baker, P. Bristow, C. Jervis, et al., ”Automatic generation of conformance tests from message sequence charts,” LNCS, 2599, 170–198 (2003). · Zbl 1024.68628
[7] B. Mitchell, R. Thomson, C. Jervis, et al., ”Phase automaton for requirements scenarios,” in: Proc. of Feature Interactions in Telecommunications and Software Systems, VII, S. l, IOS Press (2003), pp. 77–87.
[8] M. Bozga, J. C. Fernandez, L. Ghirvth, et al., ”IF: An intermediate representation for SDL and its applications,” in: Proc. 9th SDL Forum (Montreal, Quebec, Canada), Montreal (1999), pp. 423–430.
[9] F. Regensburger and A. Barnard, ”Formal verification of SDL systems at the Siemens mobile phone department,” LNCS, 1384, 439–455 (1998).
[10] O. Shumsky and L. J. Henschen, ”Developing a framework for verification, simulation, and testing of SDL specifications,” in: M. Kaufmann and J. S. Moore (eds.), Proc. ACL2 Workshop (Univ. of Texas at Austin, 2000), http://www.cs.utexas.edu/users/moore/acl2/workshop-000/final/shumsky/slides.ppt.
[11] J. Hooman, ”Towards formal support for UML-based development of embedded systems,” in: Proc. 3d PROGRESS Workshop on Embedded Systems (2002), pp. 71–76.
[12] Yu. V. Kapitonova, A. A. Letichevsky, and S. V. Konozenko, ” Computations in APS,” Theoret. Comp. Sci., 119, 145–171 (1993). · Zbl 0783.68064 · doi:10.1016/0304-3975(93)90343-R
[13] A. A. Letichevsky, Yu. V. Kapitonova, V. A. Volkov, et al., ” Insertion programming,” Cybernetics and System Analysis, 39, 16–26 (2003). · Zbl 1040.68025 · doi:10.1023/A:1023812824070
[14] S. Baranov, C. Jervis, V. Kotlyarov, et al., ”Leveraging UML to deliver correct telecom applications, ” in: L. Lavagno, G. Martin, and B. Selic (eds.), UML for Real: Design of Embedded Real-Time Systems, Kluwer, Norwell (2003), pp. 323–342.
[15] A. Letichevsky, Yu. Kapitonova, A. Letichevsky Jr., et al., ”Basic protocols, message sequence charts, and the verification of requirements specifications,” in: Proc. ISSRE 2004, WITUL (Workshop on Integrated Reliability with Telecommunications and UML Languages) (2005), http://www.sdl-forum.org/issre04-witul/papers/litechevskiweigert.pdf. · Zbl 1101.68375
[16] A. A. Letichevsky and D. R. Gilbert, ”A model for interaction of agents and environments,” LNCS, 1827, 11–32 (1999).
[17] R. Milner, Communication and Concurrency, Prentice Hall, New York (1989).
[18] C. A. R. Hoare, Communicating Sequential Processes, Prentice Hall, Englewood Cliffs (1985). · Zbl 0637.68007
[19] J. A. Bergstra and J. W. Klop, ”Process algebra for synchronous communication,” Inform. and Control, 60, 109–137 (1984). · Zbl 0597.68027 · doi:10.1016/S0019-9958(84)80025-X
[20] J. A. Bergstra, A. Ponse, and S. A. Smolka (eds.), Handbook of Process Algebra, Elsevier, Amsterdam (2001). · Zbl 0971.00006
[21] D. R. Gilbert and A. A. Letichevsky, ”A universal interpreter for nondeterministic concurrent programming languages,” in: Proc. 5th Compulog Network Area Meeting on Language Design and Semantic Analysis Methods (1996).
[22] E. M. Clarke and B.-H. Schlingloff, Model Checking: A Handbook on Automatic Reasoning, Vol. 2, Chap. 24, 1635–1790, Elsevier Sci., Amsterdam (2000).
[23] E. M. Clarke, O. Grumberg, and O. E. Long, ”Model checking and abstraction,” ACM Trans. Programming Languages and Systems, 16, 1512–1542 (1994). · doi:10.1145/186025.186051
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.