System verification is one of the main topics of interest in formal methods. In this paper, we especially focus on equivalence proofs between abstract specification and more concrete ones. We propose an encoding into PVS of an integrated specification language. This language integrates the CCS process algebra extended to manage algebraic terms written from datatype definitions. Such an integrated language is useful to specify large size systems and to cover the different involved aspects. This encoding makes it possible the use of PVS for verification of nontrivial systems. © Springer-Verlag 2003.
CITATION STYLE
Salaün, G., & Attiogbé, C. (2003). Formalising an Integrated Language in PVS. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2885, 187–205. https://doi.org/10.1007/978-3-540-39893-6_12
Mendeley helps you to discover research relevant for your work.