Developing model-checking mechanisms for ASSL: an experience report
作者： Emil Vassev , Mike Hinchey
DOI: 10.1007/978-3-642-24690-6_3
关键词: Code generation 、 Formal specification 、 Model checking 、 Software engineering 、 Consistency (database systems) 、 Formal methods 、 Computer science 、 Correctness 、 Autonomic computing 、 System requirements specification 、 Programming language
摘要: The Autonomic System Specification Language (ASSL) is a formal method dedicated to autonomic computing, and as such, assists developers with specification, validation code generation of systems. Due the synthesis approach automatic generation, ASSL guarantees consistency between specification corresponding implementation. Moreover, one major objectives framework assure correctness systems via inclusion tools targeting model checking. In this paper, we report our experience in developing model-checking mechanisms for ASSL.
springer.com
core.ac.uk 
sci-hub.st 参考文章(16)
Gerard Holzmann, Spin model checker, the: primer and reference manual Addison-Wesley Professional. ,(2003)
Emil Iordanov Vassev, Joey Paquet, Towards a framework for specification and code generation of automatic systems Concordia University. ,(2008)
Joost-Pieter Katoen, Christel Baier, Principles of Model Checking (Representation and Mind Series) The MIT Press. ,(2008)
Joost-Pieter Katoen, Christel Baier, Principles of Model Checking ,(2008)
Dexter Kozen, Results on the Propositional µ-Calculus international colloquium on automata, languages and programming. pp. 348- 359 ,(1982) , 10.1007/BFB0012782
Matthew Hennessy, Robin Milner, On Observing Nondeterminism and Concurrency international colloquium on automata, languages and programming. pp. 299- 309 ,(1980) , 10.1007/3-540-10003-2_79
Emil Vassev, Aaron J. Quigley, Mike Hinchey, Model checking for autonomic systems specified with ASSL nasa formal methods. pp. 16- 25 ,(2009)
Marco Bakera, Christian Wagner, Tiziana Margaria, Emil Vassev, Mike Hinchey, Bernhard Steffen, Component-oriented behavior extraction for autonomic system design nasa formal methods. pp. 66- 75 ,(2009)
Gerard Holzmann, The SPIN Model Checker: Primer and Reference Manual Addison-Wesley. ,(2011)
Marco Bakera, Tiziana Margaria, Clemens D. Renner, Bernhard Steffen, Game-Based Model Checking for Reliable Autonomy in Space Journal of Aerospace Computing Information and Communication. ,vol. 8, pp. 100- 114 ,(2011) , 10.2514/1.32013