Generation of multi-formalism state-space analysis tools

ABSTRACT

As software evolves from early architectural sketches to final code, a variety of representations are appropriate. Moreover, at most points in development, different portions of a software system are at different stages in development, and consequently in different representations. State-space analysis techniques (reachability analysis, model checking, simulation, etc.) have been developed for several representations of concurrent systems, but each tool or technique has typically been targeted to a single design or program notation.We describe an approach to constructing space analysis tools using a core set of basic representations and components. Such a tool generation approach differs from translation to a common formalism. We need not map every supported design formalism to a single internal form that completely captures the original semantics; rather, a shared "inframodel" represents only the essential information for interpretation by tool components that can be customized to reflect the semantics of each formalism. This results in more natural and compact internal representations, and more efficient analysis, than a purely translational approach.We illustrate the approach by applying the prototype tool to a small example problem, coordination of access to a coffee machine. The coffee machine is controlled by an Ada program, and the protocol of human users is modeled with Petri nets. Nets and process graph models are represented in the common internal form, and their composite behavior is analyzed by the prototype tool.

REFERENCES

• DAW88: Laura K. Dillon , George S. Avrunin , Jack C. Wileden, Constrained expressions: toward broad applicability of analysis methods for distributed software systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.3, p.374-402, July 1988 [doi>10.1145/44501.44502]
• GM87: Carlo Ghezzi and Dino Mandnoh On eclectlcmm m specifications A case study centered around petn nets. In ?roceed,ngs gth Internat~onaI Workshop on Software Specification and Design, pages 216-225, Monterey, April 1987 IEEE Computer Socmty.
• Rei85: Wolfgang Remlg. Pert, Nets. EATCS Monographs on Theoretical Computer Science Sprmger-Verlag, 1985
• REmP93: Raino Lintulampi Ren~ Elmstr0 m and Mauro Pezz~ Glvmg Semantics to SA/RT by Means of High Level Timed Petn Nets Journal of Real-Tame Systems, 5(2/3)'249- 272, May 1993
• RR92: Martin Richard , Olivier Roux, An Attempt to Confront Asynchronous Reality to Synchronous Modelization in the ESTEREL Language, Proceedings of the Second International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, p.429-450, January 08-10, 1992
• San89: B. Sanden, The Case for Electric Design of Real-Time Software, IEEE Transactions on Software Engineering, v.15 n.3, p.360-362, March 1989 [doi>10.1109/32.21764]
• YY91: W~i Jen Yeh and Mmhal Young Compositional teachability analyms usmg process algebra In Proceedmgs of the Symposium on Software Testmg, Analys~s, and Verification (TAVg), pages 49-59, Vlctorm, British Columbia, October 1991 ACM SIGSOFT, ACMPress
• YY94: Wei Jen Yeh and Michal Young. Redesigning tasking structures of Ada programs for analysis A case study Software Testing, Verification, and Rehab~hty, 4 223- 253, December 1994.
• Zav89: Pamela Zave, A Compositional Approach to Multiparadigm Programming, IEEE Software, v.6 n.5, p.15-25, September 1989 [doi>10.1109/52.35586]
• ZJ93: Pamela Zave , Michael Jackson, Conjunction as composition, ACM Transactions on Software Engineering and Methodology (TOSEM), v.2 n.4, p.379-411, Oct. 1993 [doi>10.1145/158431.158438]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.9 Management
          Subjects: Life cycle

General Terms:
Design, Management