Abstract
The problem is treated with a method whose main concern is the formal verification of key properties of a design. Availability of largely automatic verification procedures is, for this purpose, considered the most important point, less emphasis is put on completeness of the specification. Another distinguishing characteristic of this solution is the rôle of the remote procedure call protocol. Any implementation of the protocol must include some mechanism to ensure responsiveness. To obtain specifications of components which can be implemented independently, something must be known about the protocol mechanism. So, appropriate assumptions are made explicitly, here. These of course enter the specification and verification process.
Technically, the specification is done in an assumption/commitment variant of CTL. The verification methodology for this logic combines model checking, compositional reasoning and abstraction techniques. It indeed relies to a large extent on automatic procedures and is supported in a prototype tool, which has been used to verify partially an implementation.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. In 5th IEEE Symp. on Logic in Comp. Sc., pages 428–439, 1990.
J. Bohn and H. Hungar. Traverdi — transformation and verification of distributed systems. In M. Broy and S. Jähnichen, editors, KORSO: Methods, Languages, and Tools for the Construction of Correct Software, LNCS 1009, pages 317–338. Springer, 1995.
M. Broy and L. Lamport. The RPC-Memory Specification problem. This volume.
Jorge Cuellar, Dieter Barnard, and Martin Huber. A Solution Relying on the Model Checking of Boolean Transition Systems. This volume.
E.M. Clarke and E.A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In D. Kozen, editor, Workshop on Logics of Programs, LNCS 131, pages 52–71. Springer, 1981.
E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications. In POPL10, pages 117–126, 1983. also appeared in ACM Transact. on Prog. Lang. and Systems 8, 244–263, 1986.
E.M. Clarke, O. Grumberg, and D.E. Long. Model checking and abstraction. ACM Trans. on Prog. Lang. and Systems, 16:1512–1542, 1994.
W. Damm, G. Döhmen, R. Herrmann, P. Kelb, H. Pargmann, and R. Schlör. Verification flow. In C.D. Kloos, J. Goicolea, and W. Damm, editors, Formal Methods for Hardware Verification. Springer, 1996. to appear.
W. Damm, B. Josko, and R. Schlör. Specification and verification of VHDL-based system-level hardware designs. In E. Börger, editor, Specification and Validation Methods, pages 331–410. Oxford Univ. Press, 1995.
O. Grumberg and D.E. Long. Model checking and modular verification. ACM Trans. on Prog. Lang. and Systems, 16:843–871, 1994. Extended version of GrLo91.
H. Hungar. Combining model checking and theorem proving to verify parallel processes. In C. Courcoubetis, editor, 5th Int. Conf. on Computer Aided Verification, LNCS 697, pages 154–165. Springer, 1993.
INMOS Ltd. OCCAM 2 Reference Manual. Prentice Hall, 1988.
B. Josko. Modular specification and verification of reactive systems. Technical report, CvO Univ. Oldenburg, 1993. Habilitation Thesis.
Nils Klarlund, Mogens Nielsen, and Kim Sunesen. A Case Study in Verification Based on Trace Abstractions. This volume.
O. Kupfermann and M.Y. Vardi. On the complexity of branching modular model checking. In I. Lee and S.A. Smolka, editors, 6th Int. Conf. on Concurrency Theory, LNCS 962, pages 408–422. Springer, 1995.
Kim G. Larsen, Bernhard Steffen, and Carsten Weise. The Methodology of Modal Constraints. This volume.
Z. Manna and A. Pnueli. The temporal logic of reactive and concurrent systems: Specification. Springer, 1991.
P. Wolper. Expressing interesting properties of programs in propositional temporal logic. In 13th ACM Symp. on Principles of Programming Languages, pages 184–193, 1986.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hungar, H. (1996). Specification and verification using a visual formalism on top of temporal logic. In: Broy, M., Merz, S., Spies, K. (eds) Formal Systems Specification. Lecture Notes in Computer Science, vol 1169. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0024434
Download citation
DOI: https://doi.org/10.1007/BFb0024434
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61984-0
Online ISBN: 978-3-540-49573-4
eBook Packages: Springer Book Archive