Abstract
COSPAN (Coordination Specification Analizer [AKS83]) is an algorithmic computer-aided verification system. It's semantic model [Ku94] is founded on ω-automata: for a process P (modelling a system to be verified) and a task T which P is intended to perform, verification consists of the automata language containment test
If the test fails, COSPAN presents an error track which illustrates the error. Typically, P is not monolithic, but is represented as a (“synchronous”) parallel composition P=P 1⊗...⊗P k of component processes (all modelled as ω-automata). Asynchronous coordination of component processes may be modelled through nondeterminism in the components. The process model can be set either to Mealy or Moore machines.
COSPAN has been used on commercial applications for over a decade, both for software and hardware design verification [HK90]. Recently, it has been implemented as the “verification engine” in the commercial hardware verification tool FormalCheckTM, which is supported for hardware verification by the Bell Labs Design Automation center.
The COSPAN application domains and utilities are enumerated.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
S. Aggarwal, R. P. Kurshan, D. Sharma, A Language for the Specification and Analysis of Protocols, PSTV III, North-Holland (1983) 35–50.
R. Alur, A. Itai, R. P. Kurshan, M. Yannakakis, Timing Verification by Successive Approximation, LNCS 663 (1993) 137–150.
E. M. Clarke, E. A. Emerson, Design and Synthesis of Synchronization Skeletons for Branching Time Temporal Logic, LNCS 131 (1982) 52–71.
E. A. Emerson, C. L. Lei, Efficient Model Checking in Fragments of the Prepositional Mu-Calculus, LICS 1986, 267–278.
S. J. Garland, J. V. Guttag, A Guide to LP: the Larch Prover, Technical Report 82, Digital Equipment Corporation, 1991.
M. Gordon, A Proof-Generating System for Higher-Order Logic, Kluwer SECS 35, 1988, 73–128.
D. Gries, Describing an Algorithm by Hopcroft, Acta Inf. 2 (1973) 97–109.
R. H. Hardin, R. P. Kurshan, J. A. Reeds, N. J. A. Sloane, Regression Verification, Bell Laboratories TM11272-960502-14 (1996).
Z. Har'El, R. P. Kurshan, Software for Analytical Development of Communications Protocols, AT&T Tech. J. 69 (1990) 45–59.
G. J. Holzmann, Design and Validation of Computer Protocols, Prentice Hall, 1991.
A. Aziz, et. al, HSIS: A BDD-Based Environment for Formal Verification, Proc. 31st Design Automation Conf., 1994.
R. P. Kurshan, Computer-aided Verification of Coordinating Processes — The Automata-Theoretic Approach, Princeton Univ. Press, 1994.
L. Lamport, The temporal logic of actions, TOPLAS 16 (1994) 872–923.
K. L. McMillan, Symbolic Model Checking, Kluwer, 1993.
R. E. Tarjan, Depth-First Search and Linear Graph Algorithms, SIAM J. Comput. 1 (1972) 146–160.
P. Wolper, D. Leroy, Reliable Hashing Without Collision Detection, Lecture Notes in Computer Science (LNCS) 697 (1993) 59–70.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hardin, R.H., Har'El, Z., Kurshan, R.P. (1996). COSPAN. In: Alur, R., Henzinger, T.A. (eds) Computer Aided Verification. CAV 1996. Lecture Notes in Computer Science, vol 1102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61474-5_94
Download citation
DOI: https://doi.org/10.1007/3-540-61474-5_94
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61474-6
Online ISBN: 978-3-540-68599-9
eBook Packages: Springer Book Archive