Towards verifying safety properties of real-time probabilistic systems

Han, F, Blech, J, Herrmann, P and Schmidt, H 2014, 'Towards verifying safety properties of real-time probabilistic systems', in Bara Buhnova, Lucia Happe and Jan Kofron (ed.) Proceedings 11th International Workshop on Formal Engineering approaches to Software Components and Architectures, Grenoble, France, 12th April 2014, pp. 1-15.


Document type: Conference Paper
Collection: Conference Papers

Title Towards verifying safety properties of real-time probabilistic systems
Author(s) Han, F
Blech, J
Herrmann, P
Schmidt, H
Year 2014
Conference name 11th International Workshop on Formal Engineering approaches to Software Components and Architectures
Conference location Grenoble, France
Conference dates 12th April 2014
Proceedings title Proceedings 11th International Workshop on Formal Engineering approaches to Software Components and Architectures
Editor(s) Bara Buhnova, Lucia Happe and Jan Kofron
Publisher Electronic Proceedings in Theoretical Computer Science
Place of publication Australia
Start page 1
End page 15
Total pages 15
Abstract Using probabilities in the formal-methods-based development of safety-critical software has quickened interests in academia and industry. We address this area by our model-driven engineering method for reactive systems SPACE and its tool-set Reactive Blocks that provide an extension to support the modeling and verification of real-time behaviors. The approach facilitates the composition of system models from reusable building blocks as well as the verification of functional and real-time properties and the automatic generation of Java code. In this paper, we describe the extension of the tool-set to enable the modeling and verification of probabilistic real-time system behavior with the focus on spatial properties that ensure system safety. In particular, we incorporate descriptions of probabilistic behavior into our Reactive Blocks models and integrate the model checker PRISM which allows to verify that a real-time system satis- fies certain safety properties with a given probability. Moreover, we consider the spatial implication of probabilistic system specifications by integrating the spatial verification tool BeSpaceD and give an automatic approach to translate system specifications to the input languages of PRISM and BeSpaceD. The approach is highlighted by an example.
Subjects Software Engineering
DOI - identifier 10.4204/EPTCS.147
ISSN 2075-2180
Versions
Version Filter Type
Altmetric details:
Access Statistics: 135 Abstract Views  -  Detailed Statistics
Created: Thu, 16 Jun 2016, 10:42:00 EST by Catalyst Administrator
© 2014 RMIT Research Repository • Powered by Fez SoftwareContact us