Contract-based verification of simulink models
作者： Pontus Boström
DOI: 10.1007/978-3-642-24559-6_21
关键词: Software verification 、 High-level verification 、 Computer science 、 Functional verification 、 Verification and validation of computer simulation models 、 Runtime verification 、 Programming language 、 Intelligent verification 、 Verification 、 Correctness
摘要: This paper presents an approach to compositional contractbased verification of Simulink models. The uses Synchronous Data Flow (SDF) graphs as a formalism obtain sequential program statements that can then be analysed using traditional refinement-based techniques. Automatic generation the proof obligations needed for correctness with respect contracts, well automatic proofs are also discussed.
springer.com
acm.org 
sci-hub.st 参考文章(24)
Leonardo de Moura, Nikolaj Bjørner, Z3: an efficient SMT solver tools and algorithms for construction and analysis of systems. pp. 337- 340 ,(2008) , 10.1007/978-3-540-78800-3_24
Ralph-Johan J. Back, D. Gries, F. B. Schneider, Refinement Calculus: A Systematic Introduction ,(1998)
Ana Cavalcanti, Phil Clayton, Colin O’Halloran, Control Law Diagrams in Circus FM 2005: Formal Methods. pp. 253- 268 ,(2005) , 10.1007/11526841_18
RJR Back, Joakim von Wright, None, Trace Refinement of Action Systems international conference on concurrency theory. pp. 367- 384 ,(1994) , 10.1007/978-3-540-48654-1_28
R. J. R. Back, J. Wright, Refinement calculus, part I: Sequential nondeterministic programs Lecture Notes in Computer Science. ,vol. 430, pp. 42- 66 ,(1990) , 10.1007/3-540-52559-9_60
Rajeev Alur, Kousha Etessami, P. Madhusudan, A Temporal Logic of Nested Calls and Returns tools and algorithms for construction and analysis of systems. ,vol. 2988, pp. 467- 481 ,(2004) , 10.1007/978-3-540-24730-2_35
Bertrand Meyer, Object-Oriented Software Construction, 2nd Edition Prentice-Hall. ,(1997)
Pontus Boström, Lionel Morel, Design and Validation of Digital Controllers for Hydraulic Systems Tenth Scandinavian International Conference on Fluid Power. pp. 1- ,(2007)
Pontus Boström, Lionel Morel, Marina Waldén, Stepwise development of simulink models using the refinement calculus framework international colloquium on theoretical aspects of computing. pp. 79- 93 ,(2007) , 10.1007/978-3-540-75292-9_6
Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, K. Rustan M. Leino, Boogie: a modular reusable verifier for object-oriented programs formal methods. pp. 364- 387 ,(2005) , 10.1007/11804192_17