1,721,027 research outputs found
Explicit Algorithms for Probabilistic Model Checking
No full textIn this Thesis we present two explicit algorithms for the verification of finite horizon properties of Probabilistic Systems modeled by Discrete Time Markov Chains.
The first algorithm deals with finite horizon safety properties only. Thus, given a Markov Chain M and an integer k (horizon), this algorithm is able to check whether the probability of reaching an error state of M in at most k steps is below a given threshold.
On the other hand, the second algorithm is able to handle generic BPCTL (Bounded PCTL) formulas, i.e. PCTL formulas in which all Until operators are bounded, possibly with different bounds. This entails that we consider only system runs (paths) of bounded length. Thus, given a Markov Chain M and a BPCTL formula F, our algorithm checks if F is satisfied in M. This allows to verify important properties, which is not possible to check with the first algorithm, such as e.g. robustness in Discrete Time Stochastic Hybrid Systems.
We present an implementation of our algorithms within a suitable extension of the Murphi verifier. We call FHP-Murphi (Finite Horizon Probabilistic Murphi) such extension of the Murphi verifier.
Finally, we give experimental results comparing FHP-Murphi with PRISM, a state-of-the-art symbolic model checker for Markov Chains. Our experimental results show that FHP-Murphi can effectively handle verifications for systems that are out of reach for PRISM, namely those involving arithmetic operations on the state variables. However, PRISM is a more general verifier than Murphi, since it handles also other Markov Chain based models, and is able to verify also unbounded PCTL formulas
Formal verification at system level
No full textSystem Level Analysis calls for a language comprehensible to experts with different background and yet precise enough to support meaningful analyses. SysML is emerging as an effective balance between such conflicting goals. In this paper we outline some the results obtained as for SysML based system level functional formal verification by an ESA/ESTEC study, with a collaboration among INTECS and La Sapienza University of Roma. The study focuses on SysML based system level functional requirements techniques
Linear Constraints as a Modeling Language for Discrete Time Hybrid Systems
No full textModel Based Design is particularly appealing in embedded software design where system level specifications are much easier to define than the control software behavior itself. Formal analysis of Embedded Systems requires modelling both continuous systems (typically, the plant) as well as discrete systems (the controller). This is typically done using Hybrid Systems. Mixed Integer Linear Programming (MILP) based abstraction techniques have been successfully applied to automatically synthesize correct-by-construction control software for Discrete Time Linear Hybrid System, where plant dynamics is modeled as a linear predicate over state, input, and next state variables. MILP solvers requires constraints represented as conjunctive predicates. In this paper we show that, under the hypothesis that each variable ranges over a bounded interval, any linear predicate built upon conjunction and disjunction of linear constraints can be automatically transformed into an equisatisfiable conjunctive predicate. Moreover, since variable bounds play a key role in this transformation, we present an algorithm that taking as input a linear predicate, computes implicit variable bounds
Linear Constraints and Guarded Predicates as a Modeling Language for Discrete Time Hybrid Systems
No full textModel based design is particularly appealing in
software based control systems (e.g., embedded
software) design, since in such a case system
level specifications are much easier to define
than the control software behavior itself. In
turn, model based design of embedded systems
requires modeling both continuous subsystems
(typically, the plant) as well as discrete
subsystems (the controller). This is typically
done using hybrid systems. Mixed Integer Linear
Programming (MILP) based abstraction techniques
have been successfully applied to automatically
synthesize correct-by-construction control
software for discrete time linear hybrid systems,
where plant dynamics is modeled as a linear
predicate over state, input, and next state
variables. Unfortunately, MILP solvers require
such linear predicates to be conjunctions of
linear constraints, which is not a natural way of
modeling hybrid systems. In this paper we show
that, under the hypothesis that each variable
ranges over a bounded interval, any linear
predicate built upon conjunction and disjunction
of linear constraints can be automatically
translated into an equivalent conjunctive
predicate. Since variable bounds play a key role
in this translation, our algorithm includes a
procedure to compute all implicit variable bounds
of the given linear predicate. Furthermore, we
show that a particular form of linear predicates,
namely guarded predicates, are a natural and
powerful language to succinctly model discrete
time linear hybrid systems dynamics. Finally, we
experimentally show the feasibility of our
approach on an important and challenging case
study taken from the literature, namely the
multi-input Buck DC-DC Converter. As an example,
the guarded predicate that models (with 57
constraints) a 6-inputs Buck DC-DC Converter is
translated in a conjunctive predicate (with 102
linear constraints) in about 40 minutes
QKS
No full textQKS is an available at http://mclab.di.uniroma1.it. It is a software tool for the automatic synthesis of quantized feedback control software from the plant model and formal closed loop specifications
SyLVaaS
No full textThe goal of System Level Formal Verification is to show system correctness notwithstanding uncontrollable events (disturbances), as for example faults, variation in system parameters, external inputs, etc. This may be achieved with an exhaustive Hardware In the Loop Simulation based approach, by considering all relevant scenarios in the System Under Verification (SUV) operational environment.
SyLVaaS is a Web-based tool enabling Verification as a Service (VaaS). SyLVaaS implements an assume-guarantee approach to the verification problem outlined above. SyLVaaS takes as input a high-level model defining the SUV operational environment and computes, using parallel algorithms deployed in a cluster infrastructure, a set of highly optimised simulation campaigns, which can be executed in an embarrassingly parallel fashion on a set of Simulink instances, using a platform independent Simulink driver downloadable from the SyLVaaS
Web site. As the actual simulation is carried out at the user premises (e.g., in a private cluster), SyLVaaS allows full Intellectual Property protection on the SUV model and the user verification flow.
The simulation campaigns computed by SyLVaaS randomise the verification order of operational scenarios and this enables, at anytime during the parallel simulation activity, the estimation of the completion time and the computation of an upper bound to the Omission Probability, i.e., the probability that there is a yet-to-be-simulated operational scenario which violates the property under verification. This information supports graceful degradation in the verification activity
Control Software Visualization
No full textMany software as well digital hardware automatic
synthesis methods define the set of
implementations meeting the given system
specifications with a boolean relation K
(controller). Such relation, given a system state
s and an action u, returns 1 iff taking action u
in state s leads in the system goal or at least
one step closer to it. In order to determine at
hand if K is a "good" controller, e.g., if it
covers a wide enough portion of the system state
space, or to provide an high level view of the
actions enabled by K, it is useful to picture K in
a 2D or 3D diagram. In this paper, starting from a
canonical representation for K, we propose an
algorithm to automatically generate such a
picture, relying on available graphing tools
- …
