Search

International audience; Probabilistic veri cation techniques have been proposed for runtime analysis of adaptive software systems, with the veri cation results being used to steer the system so that it satis es certain Quality-of-Service requirements. Since systems evolve over time, and veri cation results are required promptly, e ciency is an essential issue. To address this, we present incremental veri cation techniques, which exploit the results of previous analyses. We target systems modelled as Markov decision processes, developing incremental methods for constructing models from high-level system descriptions and for numerical solution using policy iteration based on strongly connected components. A prototype implementation, based on the PRISM model checker, demonstrates performance improvements on a range of case studies.

We report on a novel approach to (semi-)automatically compile and verify contract-regulated service compositions implemented as multi-agent systems. We model web service behaviours and the contracts governing them as WSBPEL specification. We use the formalism of temporal-epistemic logic, suitably extended to deal with compliance/violations of contracts, to specify properties of service compositions. We compile the WSBPEL behaviours into a specialised system description language ISPL, to be used with the model checker MCMAS to verify the behaviours automatically. We illustrate these concepts using a motivating example whose state space is approximately 106 and discuss experimental results.

Quantitative verification techniques offer an effective meansof computing performance and reliability properties for a wide range of systems.In many cases, it is necessary to perform repeated analyses of a system,for example to identify trends in results, determine optimal system parametersor when performing online analysis for adaptive systems.We argue the need for incremental quantitative verification techniqueswhich are able to re-use results from previous verification runs in order to improve efficiency.We report on recently proposed techniques for incremental quantitative verification of Markov decision processes,based on a decomposition of the model into its strongly connected components.We give an overview of the method, describe a number of useful optimisationsand show experimental results that illustrate significant gains in run-time performanceusing the incremental approach.

International audience; Fairness assumptions are needed to verify liveness properties of concurrent systems. In this paper we explore the so-called unconditional fairness in Markov decision processes (MDPs), which is a prerequisite for quantitative assume- guarantee reasoning. Unconditional fairness refers to execu- tions where all processes are guaranteed to participate. We prove that realisability of unconditional fairness coincides with the absence of partial deadlocks, i.e., end components where a process suffers from starvation. We propose a weak variant of the stubborn set method to reduce MDPs, while preserving the realisability of unconditional fairness and maximal probabili- ties of reaching bottom end components under fair schedulers.

International audience; Quantitative verification techniques provide an effective means of computing performance and reliability properties for a wide range of systems. However, the com- putation required can be expensive, particularly if it has to be performed multiple times, for example to determine optimal system parameters. We present efficient incremental techniques for quantitative verification of Markov decision processes, which are able to re-use results from previous verification runs, based on a decomposition of the model into its strongly connected components (SCCs). We also show how this SCC-based approach can be further optimised to improve verification speed and how it can be combined with symbolic data structures to offer better scalability. We illustrate the effectiveness of the approach on a selection of large case studies.

We present an automatic data-abstraction technique for the verification of the universal fragment of the temporal-epistemic logic CTLK. We show the correctness of the methodology and present an implementation operating on ISPL models, the input files for MCMAS, a model checker for multi-agent systems. The experimental results point to the attractiveness of the technique in a number of examples in the multi-agent systems domain.

International audience; We present a verification framework for analysing multiple quantitative objectives of systems that exhibit both nondeterministic and stochastic behaviour. These systems are modelled as probabilistic automata, enriched with cost or reward structures that capture, for ex- ample, energy usage or performance metrics. Quantitative properties of these models are expressed in a specification language that incorporates probabilistic safety and liveness properties, expected total cost or re- ward, and supports multiple objectives of these types. We propose and implement an efficient verification framework for such properties and then present two distinct applications of it: firstly, controller synthesis subject to multiple quantitative objectives; and, secondly, quantitative compositional verification. The practical applicability of both approaches is illustrated with experimental results from several large case studies.

International audience; The Connect project aims to enable the seamless composition of heterogeneous networked systems. In this context, Verication and Validation (V&V) techniques are sought to ensure that the Con- nected system satises dependability requirements. Stochastic model checking and state-based stochastic methods are two appealing V&V approaches to accomplish this task. In this paper, we report on the application of the two approaches in a typical Connect scenario. Specifically, we make clear (i) how the two approaches can be employed to enhance the condence in the correctness of the analysis, and (ii) how the complementarity of these approaches can be fruitfully exploited to extend the analysis.

International audience; In this paper, we present Reo2MC, a tool chain for the performance evaluation of coordination models. Given a coordination model represented by a stochastic Reo connector, Reo2MC is able to automatically generate the Quantitative Intentional Automaton (QIA) as its operational semantics, and the corresponding Continuous- Time Markov Chain (CTMC), which allows us to apply existing CTMC tools, e.g., PRISM, for performance analysis of Reo connectors. In support of understanding connector behavior and performance properties, the tool also provides the graphical representation of the QIA and Markov Chains.

Model-based test derivation for real-time system has been proven to be a hard problem for exhaustive test suites. Therefore, techniques for real-time testing do not aim to exhaustiveness but Instead respond to particular coverage criteria. Since it Is not feasible to generate complete test suites for real time systems, It IsI very Important that test case are executed In a way that they can achieve the best possible resuIlt As a consequence, It is imperative to Increase the probabilty of success of a test case execution (by 'success' we actually mean 'the test finds an error'). This work presents a technique to guide the execution of a test case towards a particular objective with the highest possible probability. Thke technique takes as a starting point a model described In terms of an input/output stochastic automata, where input actions are fully controlled by the tester and the occurrece time of output action responds to uniform distributions. Derived test cases are sequences of Inputs and outputs actions. This work discusses several techniques to obtain the optimum times In which the tester must feed the inputs of the test case in order to achieve maxhmum probabilty of success in a test case execution. In particular~, we show this optimization problem Is equivalent to maximizing the sectional volume of a convex polytope when the probabilty distributions Involved are uniform.

We present a data symmetry reduction approach for model checking temporal-epistemic logic. The technique abstracts the epistemic indistinguishably relation for the knowledge operators, and is shown to preserve temporal-epistemic formulae. We show a method for statically detecting data symmetry in an ISPL program, the input to the temporal-epistemic model checker MCMAS. The experiments we report show an exponential saving in verification time and space while verifying security properties of the NSPK protocol.

We introduce basic partial order reduction techniques in a temporal-epistemic setting. We analyse the semantics of interpreted systems with respect to the notions of trace-equivalence for the epistemic linear time logic LTLK*** X .

While temporal logic in its various forms has proven essential to reason about reactive systems, agent-based scenarios are typically specified by considering high-level agents attitudes. In particular, specification languages based on epistemic logic [7], or logics for knowledge, have proven useful in a variety of areas including robotics, security protocols, web-services, etc. For example, security specifications involving anonymity [4] are known to be naturally expressible in epistemic formalisms as they explicitly state the lack of different kinds of knowledge of the principals.

Software verification is a hard yet important challenge. In general, the problem is undecidable. Nevertheless, it is still beneficial to look at solutions that either restrict the generality or are heuristic in nature (and do not guarantee to terminate). In this paper, we concentrate on a related problem, that of verifying that a cycle in the flow chart of a program does not terminate. We show some exact and sufficient conditions for cycle nontermination, and provide application for program verification. This allows us to check sequential and concurrent programs against temporal properties, using a truly symbolic approach, and to use temporal logic to guide the selection of test cases in such programs.

This paper presents an automatic method for calculating the path condition for programs with real time constraints. We model concurrent systems using timed transition systems and translate them into extended timed automata. Then an acyclic extended timed automaton is constructed and the path condition is calculated backwards over it. This method can be used for semiautomatic verification of a unit of code in isolation, i.e., without providing the exact values of parameters with which it is called. It can also be used for test case generation for real-time systems. Such a symbolic model checking algorithm was implemented previous in the PET system [E. Gunter, D. Peled, Unit checking: Symbolic model checking for a unit of code, Verification: Theory and Practice 2003, Essays Dedicated to Zohar Manna on the Occasion of his 64th Birthday, Lecture Notes in Computer Science, vol. 2772, Springer, 548–567] for untimed systems. Our method can also be used for the automatic generation of test cases for unit testing. The current generalization of the calculation of path condition for the timed case turns out to be quite tricky, since not only the selected path contributes to the path condition, but also timing constraints of alternative choices in the code.

Model checking Web service behaviour has remained limited to checking safety and liveness properties. However when viewed as a multi agent system, the system composition can be analysed by considering additional properties which capture the knowledge acquired by services during their interactions. In this paper we present a novel approach to model checking service composition where in addition to safety and liveness, epistemicproperties are analysed and verified. To do this we use a specialised system description language (ISPL) paired with a symbolic model checker (MCMAS) optimised for the verification of temporal and epistemic modalities. We report on experimental results obtained by analysing the composition for a Loan Approval Service.

Calculating the precondition of a particular partial-ordered set of events is often necessary in software testing, such as for generating test cases. Things become even more complicated when the execution time is added to the picture. If the execution time of two processes along a partial order does not match each other, the precondition of the partial order is false and then the partial order is identified as time unbalanced partial order. We present its formal definition and an algorithm to distinguish it. Then we suggest a method to fill the gap of the execution time of participating processes. This method can also be adopted to simplify the calculation of the minimal and maximal bounds of a time parameter.

When testing a system, it is often necessary to execute a suspicious trace in a realistic environment. Due to nondeterministic choices existing in concurrent systems, such a particular trace may not be scheduled for execution. Thus it is useful to compute the probability of executing the trace. Our probabilistic model of real-time systems requires that for each transition, the period from the time when its enabling condition becomes satisfied to the time when it is fired is bounded and the length of the period obeys a probabilistic distribution. This model is not Markovian if the distribution is not exponential. Therefore it cannot be analyzed by Markov processes. We propose to use integration to calculate the probability for a path. Then we discuss the possibility to optimize the calculation.

We present the implementation of trace theory in a new model checking tool framework, POEM, that has a strong emphasis on Partial Order Methods. A tree structure is used to store trace systems, which allows sharing common prefixes among traces and therefore reduces memory cost. This structure is easy to extend to incorporate additional features. Two applications are shown in the paper: An extended structure to support a new adequate order for Local First Search, and an acceleration of event zone based state space search for timed automata.

There are many cases where we want to verify a system that does not have a usable formal model: the model may be missing, out of date, or simply too big to be used. A possible method is to analyze the system while learning the model (black box checking). However, learning may be an expensive task, thus it needs to be guided, e.g., using the checked property or an inaccurate model (adaptive model checking). In this paper, we consider the case where some of the system components are completely specified (white boxes), while others are unknown (black boxes), giving rise to a grey box system. We provide algorithms and lower bounds, as well as experimental results for this model.

Model checking is an automatic approach for the verification of systems. Explicit states model checking applies a search algorithm (e.g., depth or breadth first search) to the state space of the verified system. In concurrent systems, and in particular in communication protocols, the number of states can grow exponentially with the number of independent components (processes). There are many different methods that attempt to automatically reduce the number of checked states. Such methods show encouraging results, but often still fail to reduce the number of states required for the verification to become manageable. We propose here the use of code annotation in order to control the verification process and reduce the number of states searched. Our extension of the C programming language allows the user to put into the code instructions that are executed by the model checker during the verification. With the new language construct, we may exploit additional insight that the verifier may have about the checked program in order to limit the search. We describe our implementation and present some experimental results.

We consider models of programs that incorporate probability, dense real-time and data. We present a new abstraction refinement method for computing minimum and maximum reachability probabilities for such models. Our approach uses strictly local refinement steps to reduce both the size of abstractions generated and the complexity of operations needed, in comparison to previous approaches of this kind. We implement the techniques and evaluate them on a selection of large case studies, including some infinite-state probabilistic real-time models, demonstrating improvements over existing tools in several cases.

The outcome of verifying software is often a 'counterexample', i.e., a listing of the actions and states of a behavior not satisfying the specification. The verification is usually done using a model of the software (often also using some abstraction to reduce its complexity) rather than the actual code. In order to understand the reason for the failure manifested by such a counterexample, it is sometimes necessary to test such an execution using the actual code. In this way we also find out whether we have a genuine error or a "false negative". Due to nondeterminism in concurrent code, enforcing a particular behavior of an actual program is not guaranteed even when one starts the execution with the prescribed initial state. Testers are faced with a similar problem when they have to demonstrate that a suspicious scenario can actually be executed. Such a scenario may involve some intricate scheduling and thus be illusive to demonstrate. We describe here a transformation that allows us to repeat a selected execution sequences of concurrent code. Since the transformation implies changes to the original code, we strive to minimize its effect on the original program.