Mechanization of an Integrated Approach: Shallow Embedding into SAL/PVS
关键词: Specification language 、 Transition system 、 Data modeling 、 State (computer science) 、 Computer science 、 Computation tree logic 、 Symbolic data analysis 、 Programming language 、 Embedding 、 Formal language
摘要: This paper describes a work on the systematic embedding into SAL of specifications written in integrated approach Configuration Machines. The final goal is to perform formal analysis. an intermediate language used as input various reasoning tools and especially PVS. Machine specification technique combining transition systems state based data models. Our technique, translation SAL, presented, formalised discussed.
archives-ouvertes.fr
springer.com
sci-hub.st 参考文章(22)
Bernd Krieg-Brückner, Jan Peleska, Ernst-Rüdiger Olderog, Alexander Baer, The UniForM Workbench, a Universal Development Environment for Formal Methods formal methods. pp. 1186- 1205 ,(1999) , 10.1007/3-540-48118-4_13
Mandayam Srivas, John Rushby, A Tutorial Introduction to PVS ,(1998)
Clemens Fischer, CSP-OZ: a combination of object-Z and CSP formal methods for open object based distributed systems. pp. 423- 438 ,(1997) , 10.1007/978-0-387-35261-9_29
Bill Stoddart, An Introduction to the Event Calculus ZUM '97 Proceedings of the 10th International Conference of Z Users on The Z Formal Specification Notation. pp. 10- 34 ,(1997) , 10.1007/BFB0027281
Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu, Susanne Graf, Jean-Pierre Krimm, Laurent Mounier, IF: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems formal methods. ,vol. 1708, pp. 307- 327 ,(1999) , 10.1007/3-540-48119-2_19
Clemens Fischer, How to Combine Z with Process Algebra ZUM '98 Proceedings of the 11th International Conference of Z Users on The Z Formal Specification Notation. pp. 5- 23 ,(1998) , 10.1007/978-3-540-49676-2_2
César Muñoz, John Rushby, Structural Embeddings: Mechanization with Method formal methods. pp. 452- 471 ,(1999) , 10.1007/3-540-48119-2_26
M. J. C. Gordon, T. F. Melham, Introduction to HOL: a theorem proving environment for higher order logic Cambridge University Press. ,(1993)
David W. J. Stringer-Calvert, Susan Stepney, Ian Wand, Using PVS to Prove a Z Refinement: A Case Study formal methods. pp. 573- 588 ,(1997) , 10.1007/3-540-63533-5_30
David L. Dill, The Murphi Verification System computer aided verification. pp. 390- 393 ,(1996)