Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userThe Probabilistic Model Checker Storm (Extended Abstract)
200
0
0.0
(
0
)
Added by
Sebastian Junges
Publication date
2016
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
We present a new probabilistic model checker Storm. Using state-of-the-art libraries, we aim for both high performance and versatility. This extended abstract gives a brief overview of the features of Storm.
rate research
Read More
We present the probabilistic model checker Storm. Storm supports the analysis of discrete- and continuous-time variants of both Markov chains and Markov decision processes. Storm has three major distinguishing features. It supports multiple input languages for Markov models, including the JANI and PRISM modeling languages, dynamic fault trees, generalized stochastic Petri nets, and the probabilistic guarded command language. It has a modular set-up in which solvers and symbolic engines can easily be exchanged. Its Python API allows for rapid prototyping by encapsulating Storms fast and scalable algorithms. This paper reports on the main features of Storm and explains how to effectively use them. A description is provided of the main distinguishing functionalities of Storm. Finally, an empirical evaluation of different configurations of Storm on the QComp 2019 benchmark set is presented.
This extended abstract reports on current progress of SMTCoq, a communication tool between the Coq proof assistant and external SAT and SMT solvers. Based on a checker for generic first-order certificates implemented and proved correct in Coq, SMTCoq offers facilities both to check external SAT and SMT answers and to improve Coqs automation using such solvers, in a safe way. Currently supporting the SAT solver zChaff, and the SMT solver veriT for the combination of the theories of congruence closure and linear integer arithmetic, SMTCoq is meant to be extendable with a reasonable amount of effort: we present work in progress to support the SMT solver CVC4 and the theory of bit vectors.
In the software development process, model transformation is increasingly assimilated. However, systems being developed with model transformation sometimes grow in size and become complex. Meanwhile, the performance of model transformation tends to decrease. Hence, performance is an important quality of model transformation. According to current research model transformation performance focuses on optimising the engines internally. However, there exists no research activities to support transformation engineer to identify performance bottleneck in the transformation rules and hence, to predict the overall performance. In this paper we vision our aim at providing an approach of monitoring and profiling to identify the root cause of performance issues in the transformation rules and to predict the performance of model transformation. This will enable software engineers to systematically identify performance issues as well as predict the performance of model transformation.
The assurance of quality of service properties is an important aspect of service-oriented software engineering. Notations for so-called service level agreements (SLAs), such as the Web Service Level Agreement (WSLA) language, provide a formal syntax to specify such assurances in terms of (legally binding) contracts between a service provider and a customer. On the other hand, formal methods for verification of probabilistic real-time behavior have reached a level of expressiveness and efficiency which allows to apply them in real-world scenarios. In this paper, we suggest to employ the recently introduced model of Interval Probabilistic Timed Automata (IPTA) for formal verification of QoS properties of service-oriented systems. Specifically, we show that IPTA in contrast to Probabilistic Timed Automata (PTA) are able to capture the guarantees specified in SLAs directly. A particular challenge in the analysis of IPTA is the fact that their naive semantics usually yields an infinite set of states and infinitely-branching transitions. However, using symbolic representations, IPTA can be analyzed rather efficiently. We have developed the first implementation of an IPTA model checker by extending the PRISM tool and show that model checking IPTA is only slightly more expensive than model checking comparable PTA.
Providing compact and understandable counterexamples for violated system properties is an essential task in model checking. Existing works on counterexamples for probabilistic systems so far computed either a large set of system runs or a subset of the systems states, both of which are of limited use in manual debugging. Many probabilistic systems are described in a guarded command language like the one used by the popular model checker PRISM. In this paper we describe how a smallest possible subset of the commands can be identified which together make the system erroneous. We additionally show how the selected commands can be further simplified to obtain a well-understandable counterexample.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
