Insertion modeling in distributed system design

A.A. Letichevsky, J.V. Kapitonova, V.P. Kotlyarov, A.A. Letichevsky Jr., N.S. Nikitchenko, V.A. Volkov, T. Weigert

Abstract


The paper describes insertion modeling methodology, its implementation and applications. Insertion modeling is a methodology of model driven distributed system design. It is based on the model of interaction of agents and environments [1-2] and use Basic Protocol Specification Language (BPSL) for the representation of requirement specifications of distributed systems [3-6]. The central notion of this language is the notion of basic protocol – a sequencing diagram with pre- and postconditions, logic formulas interpreted by environment description. Semantics of BPSL allows concrete and abstract models on different levels of abstraction. Models defined by Basic Protocol Specifications (BPS) can be used for verification of requirement specifications as well as for generation of test cases for testing products, developed on the basis of BPS.

Insertion modeling is supported by the system VRS (Verification of Requirement Specifications), developed for Motorola by Kiev VRS group in cooperation with Motorola GSG Russia. The system provides static requirement checking on the base of automatic theorem proving, symbolic and deductive model checking, and generation of traces for testing with different coverage criteria. All tools have been developed on a base of formal semantics of BPSL constructed according to insertion modeling methodology.

The VRS has been successfully applied to a number of industrial projects from different domains including Telecommunications, Telematics and real time applications.

Problems in programming 2008; 4: 13-38


Full Text:

PDF

References


Letichevsky and D. Gilbert. A Model for Interaction of Agents and Environments. In D. Bert, C. Choppy, P. Moses, editors. Recent Trends in Algebraic Development Techniques. Lecture Notes in Computer, Springer, 1999, Science 1827.

Letichevsky A. Algebra of behavior transformations and its applications, in V.B.Kudryavtsev and I.G.Rosenberg eds. Structural theory of Automata, Semigroups, and Universal Algebra, NATO Science Series II. Mathematics, Physics and Chemistry – Springer 2005. – Vol. 207, P. 241–272.

Baranov S., Jervis C., Kotlyarov V., Letichevsky A., and Weigert T. Leveraging UML to Deliver Correct Telecom Applications. In L. Lavagno, G. Martin, and B.Selic, editors. UML for Real: Design of Embedded Real-Time Systems. Kluwer Academic Publishers, Amsterdam, 2003.

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

J. Kapitonova, A. Letichevsky, V. Volkov, and T. Weigert. Validation of Embedded Systems. In R. Zurawski, editor. The Embedded Systems Handbook. CRC Press, Miami, 2005.

A.A.Letichevsky, J.V.Kapitonova, V.A.Volkov, A.A.Letichevsky, jr., S.N.Baranov, V.P.Kotlyarov, T.Weigert. System Specification with Basic Protocols, Cybernetics and System Analyses, 4, 2005.

International Telecommunications Union. Recommendation Z.120 Annex B: Formal semantics of Message Sequence Charts, 1998.

Reniers M.A. Message Sequence Chart: Syntax and Semantics. Eindhoven, University of Technology, 1998.

Letichevsky A.A., Kapitonova J.V., Kotlyarov V.P., Volkov V.A., Letichevsky A.A. Jr., and Weigert T. Semantics of Message Sequence Charts, SDL Forum, 2005.

Letichevsky A.A, Kapitonova J.V., Kotlyarov V.P., Letichevsky A.A. Jr, Volkov V.A. Semantics of timed MSC language, Kibernetika and System Analysis, 2002.

Degtyarev, J. Kapitonova, A. Letichevsky, A. Lyaletsky, and M. Morokhovets. Evidence algorithm and problems of representation and processing of computer mathematical knowledge. Kibernetika and System Analysis, (6):9–17, 1999.

C.A.R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.

R. Milner. Communication and Concurrency. Prentice Hall, 1989.

L. Lamport. Introduction to TLA. SRC Technical Note 1994-001, 1994.

L. Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, May 1994. – P. 872-923.

Pnueli. The temporal logic of programs // Proc. of the 18th Annual Symp. on the Foundations of Comp. Sci. – Nov. 1977. – P. 46–52.

E. Emerson and J. Halpern. Decision procedures and expressiveness in the temporal logic of branching time // J. of Comp. and System Sci., 1985. – 30(1):1–24.

M.J. Fisher and R. E. Ladner. Propositional modal logic of programs // Proc. 9th ACM Ann. Symp. on Theory of Comp. – Boulder, Col., May 1977. – P. 286–294.

Emerson E. Temporal and modal logic. In: J. van Leeuwen editor: Handbook of Theoretical Computer Science, Elsevier, (B):997–1072, 1990.

Bryant R. Graph-based algorithms for Boolean function anipulation // IEEE Trans. on Computers, 35 (8). – 1986. – P. 677–691.

Clarke E. and Emerson E. Synthesis of synchronization skeletons for branching time temporal logic // The Workshop on Logic of Programs, 128–143, Lecture Notes in Computer Sci., 131. Springer Verlag, 1981.

J. Quielle and J. Sifakis. Specification and verification of concurrent systems in CESAR. In: Proc. 5th Intern. Symposium on Programming , 142–158, 1981.

J. Burch, E. Clarke, K. McMillan, D. Dill, and L. Hwang. Symbolic model checking: 10^20 states and beyond. Information and Computation, 98 (2): 142–170, 1992.

Constance Heitmeyer, Myla Archer, Ramesh Bharadwaj and Ralph Jeffords/ Tools for constructing requirements specifications: The SCR toolset at the age of ten, Computer Systems Science & Engineering, 1: 19-35, 2005.

T. Bultan and T. Yavuz-Kahveci. Action language verifier. In Proc. of ASE 2001, 382– 386, November 2001.

David Harel, Rami Marelly. Come, Let’s Play: Scenario-Based programming Using LSCs and the Play-Engine. Springer 2003.

Sengupta and R. Cleaveland. Triggered Message Sequence Charts. In Proceedings of SIGSOFT 2002/FSE-10, 167–176, ACM Press, 2002.

Frank Buschmann, Regine Meunier Hans Rohnert, Peter Sommerlad, and Michael Stal. Pattern-Oriented Software Architecture-A System of Patterns. Wiley & Sons, New York, 1996.


Refbacks

  • There are currently no refbacks.