Nordic Journal of Computing Bibliography

Abstract

This paper proposes a method to construct a set of proof obligations from the architectural specification of a concurrent system. The architectural specifications used express correctness requirements of a concurrent system at a high level without any reference to component functionality. Then the proof obligations derived from such specifications are discharged as model checking tasks in a suitable behavioral model where components are assigned their respective functionalities. An experimental extension to the SPIN tool is used as the model checker. The block diagram notation used to specify architectures allows interchangeable components with equivalent intended functionalities to be encapsulated within a representative module. A proof obligation of such a system is discharged as an equivalence checking task in the behavioral model chosen. It is shown how infeasible proof obligations can be decomposed by decomposing the architectural specification. Obligation decomposition relies on assume-guarantee conditions.

Categories and Subject Descriptors: D.2.1 [Software Engineering]: Requirements/Specifications; D.2.4 [Software Engineering]: Program Verification; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs; C.2.4 [Computer-Communication Networks]: Distributed Systems

Additional Key Words and Phrases: architecture-based verification, architectural specifications, architectural formalisms, model checking, equivalence checking, compositional verification

Selected references

• Martín Abadi and Leslie Lamport. Composing specifications. ACM Transactions on Programming Languages and Systems, 15(1):73-132, January 1993.

• Martín Abadi and Leslie Lamport. Conjoining specifications. ACM Transactions on Programming Languages and Systems, 17(3):507-534, May 1995.

• Gregory D. Abowd, Robert B. Allen, and David Garlan. Formalizing style to understand descriptions of software architecture. ACM Transactions on Software Engineering and Methodology, 4(4):319-364, October 1995.

• Bard Bloom, Sorin Istrail, and Albert R. Meyer. Bisimulation can't be traced. In Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, pages 229-239, San Diego, California, January 1988.

• Edmund M. Clarke, Orna Grumberg, and David E. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5):1512-1542, September 1994.

• Thomas R. Dean and James R. Cordy. A syntactic theory of software architecture. IEEE Transactions on Software Engineering, 21(4):302-313, April 1995.

• Orna Grumberg and David E. Long. Model checking and modular verification. ACM Transactions on Programming Languages and Systems, 16(3):843-871, May 1994.

• Paola Inverardi and Alexander L. Wolf. Formal specification and analysis of software architectures using the chemical abstract machine model. IEEE Transactions on Software Engineering, 21(4):373-386, April 1995.

• Farnam Jahanian and Aloysius K. Mok. Modechart: A specification language for real-time systems. IEEE Transactions on Software Engineering, 20(12):933-947, December 1994.

• Bengt Jonsson. Modular verification of asynchronous networks. In Proceedings of the Sixth Annual ACM Symposium on Principles of Distributed Computing, pages 152-166, Vancouver, British Columbia, Canada, 10-12 August 1987.

• David C. Luckham, John J. Kenney, Larry M. Augustin, James Vera, D. Bryan, and Walter Mann. Specification and analysis of system architecture using Rapide. IEEE Transactions on Software Engineering, 21(4):336-355, April 1995.

• David C. Luckham and James Vera. An event-based architecture definition language. IEEE Transactions on Software Engineering, 21(9):717-734, September 1995.

• Nancy A. Lynch and Mark R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proceedings of the Sixth Annual ACM Symposium on Principles of Distributed Computing, pages 137-151, Vancouver, British Columbia, Canada, 10-12 August 1987.

• Mark Moriconi, Xiaolei Qian, and R. A. Riemenschneider. Correct architecture refinement. IEEE Transactions on Software Engineering, 21(4):356-372, April 1995.

• Rocco De Nicola. Extensional equivalences for transition systems. Acta Informatica, 24(2):211-237, 1987.

• R. De Nicola and M. C. B. Hennessy. Testing equivalences for processes. Theoretical Computer Science, 34(1-2):83-133, November 1984.

• Mary Shaw, Robert DeLine, Daniel V. Klein, Theodore L. Ross, David M. Young, and Gregory Zelesnik. Abstractions for software architecture and tools to support them. IEEE Transactions on Software Engineering, 21(4):314-335, April 1995.

• Sandeep K. Shukla, Harry B. Hunt III, Daniel J. Rosenkrantz, and Richard Edwin Stearns. On the complexity of relational problems for finite state processes (extended abstract). In Friedhelm Meyer auf der Heide and Burkhard Monien, editors, Automata, Languages and Programming, 23rd International Colloquium, volume 1099 of Lecture Notes in Computer Science, pages 466-477, Paderborn, Germany, 8-12 July 1996. Springer-Verlag.

Shortcuts: