dc.contributor.author | Han, Fenglin | |
dc.contributor.author | Blech, Jan Olaf | |
dc.contributor.author | Herrmann, Peter Michael | |
dc.contributor.author | Schmidt, Heinz | |
dc.date.accessioned | 2015-01-26T16:40:15Z | |
dc.date.accessioned | 2015-12-21T12:24:15Z | |
dc.date.available | 2015-01-26T16:40:15Z | |
dc.date.available | 2015-12-21T12:24:15Z | |
dc.date.issued | 2014 | |
dc.identifier.citation | Electronic Proceedings in Theoretical Computer Science 2014, 147:1-15 | nb_NO |
dc.identifier.issn | 2075-2180 | |
dc.identifier.uri | http://hdl.handle.net/11250/2368701 | |
dc.description.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 satisfies
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 Be-
SpaceD. The approach is highlighted by an example. | nb_NO |
dc.language.iso | eng | nb_NO |
dc.publisher | Open Publishing Association | nb_NO |
dc.title | Towards Verifying Safety Properties of Real-Time Probabilistic Systems | nb_NO |
dc.type | Journal article | nb_NO |
dc.type | Peer reviewed | en_GB |
dc.date.updated | 2015-01-26T16:40:15Z | |
dc.source.volume | 147 | nb_NO |
dc.source.journal | Electronic Proceedings in Theoretical Computer Science | nb_NO |
dc.identifier.doi | 10.4204/EPTCS.147.1 | |
dc.identifier.cristin | 1191054 | |
dc.description.localcode | (c) F. Han, J.O. Blech, P. Hermann, H. Schmidt. This work is licensed under the Creative Commons Attribution Licenses. | nb_NO |