Formally verified modular semantics
作者： K. Madlener
DOI:
关键词:
摘要: This chapter presents the results of validation and verification a crucial component BOS, large safety-critical system that decides when to close open Maeslantkering, storm surge barrier near city Rotterdam in Netherlands. BOS was specified formal language Z model checking has been applied some its subsystems during development. A lightweight C++ code specification manually developed theorem prover PVS. As result, essential mismatches between were identified. The itself is also validated by use challenge theorems, assess particular design choices. Tools have used exhaustively search for inconsistencies original which led deeper issues with itself.
ru.nl参考文章(68)
Filippo Bonchi, Stefan Milius, Alexandra Silva, Fabio Zanasi, Killing epsilons with a dagger: A coalgebraic study of systems with algebraic label structure Theoretical Computer Science. ,vol. 604, pp. 102- 126 ,(2015) , 10.1016/J.TCS.2015.03.024
Wan J. Fokkink, Luca Aceto, Chris Verhoef, Structural Operational Semantics. Handbook of Process Algebra. pp. 197- 292 ,(2001)
Mark Saaltink, The Z/EVES System ZUM '97 Proceedings of the 10th International Conference of Z Users on The Z Formal Specification Notation. pp. 72- 85 ,(1997) , 10.1007/BFB0027284
Thomas Tuerk, A Formalisation of Smallfoot in HOL theorem proving in higher order logics. pp. 469- 484 ,(2009) , 10.1007/978-3-642-03359-9_32
F. Bartels, On Generalised Coinduction and Probabilistic Specification Formats ,(2004)
Peter D. Mosses, Teaching semantics of programming languages with modular SOS formal methods. pp. 12- 12 ,(2006) , 10.14236/EWIC/TFM2006.12
Martin Churchill, Peter D. Mosses, Modular bisimulation theory for computations and values foundations of software science and computation structure. pp. 97- 112 ,(2013) , 10.1007/978-3-642-37075-5_7
Bart Jacobs, Introduction to Coalgebra: Towards Mathematics of States and Observation ,(2016)
Keiko Nakata, Tarmo Uustalu, A hoare logic for the coinductive trace-based big-step semantics of while european symposium on programming. pp. 488- 506 ,(2010) , 10.1007/978-3-642-11957-6_26
R. M. Burstall, Some Techniques for Proving Correctness of Programs which Alter Data Structures ,(2013)