Contract-based verification of discrete-time multi-rate Simulink models
作者： Pontus Boström , Jonatan Wiik
DOI: 10.1007/S10270-015-0477-X
关键词:
摘要: This paper presents an approach to modular contract-based verification of discrete-time multi-rate Simulink models. The uses a translation models sequential programs that can then be verified using traditional software techniques. Automatic generation the proof obligations needed for correctness with respect contracts, and automatic proofs are also discussed. Furthermore, provides detailed discussions about each step in process. is demonstrated on case study involving control prevention pressure peaks hydraulics systems.
springer.com
sci-hub.se 参考文章(43)
Robert Reicherdt, Sabine Glesner, Formal Verification of Discrete-Time MATLAB/Simulink Models Using Boogie international conference on software engineering. pp. 190- 204 ,(2014) , 10.1007/978-3-319-10431-7_14
Pierre-Loïc Garoche, Temesghen Kahsai, Cesare Tinelli, Incremental Invariant Generation Using Logic-Based Automatic Abstract Transformers nasa formal methods symposium. pp. 139- 154 ,(2013) , 10.1007/978-3-642-38088-4_10
Pontus Boström, Contract-based verification of simulink models formal methods. pp. 291- 306 ,(2011) , 10.1007/978-3-642-24559-6_21
Jonatan Wiik, Pontus Boström, Contract-Based Verification of MATLAB and Simulink Matrix-Manipulating Code international conference on formal engineering methods. pp. 396- 412 ,(2014) , 10.1007/978-3-319-11737-9_26
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
Mary Sheeran, Satnam Singh, Gunnar Stålmarck, Checking Safety Properties Using Induction and a SAT-Solver formal methods in computer aided design. pp. 108- 125 ,(2000) , 10.1007/3-540-40922-X_8
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
K. Rustan M. Leino, Peter Müller, A verification methodology for model fields european symposium on programming. pp. 115- 130 ,(2006) , 10.1007/11693024_9
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