89 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
Model Based Synthesis of Control Software from System Level Formal Specifications
No full textMany Embedded Systems are indeed Software Based Control
Systems, that is control systems whose controller consists
of control software running on a microcontroller device.
This motivates investigation on Formal Model Based Design
approaches for automatic synthesis of embedded systems
control software.
We present an algorithm, along with a tool QKS implementing
it, that from a formal model (as a Discrete Time Linear
Hybrid System) of the controlled system (plant),
implementation specifications (that is, number of bits in
the Analog-to-Digital, AD, conversion) and System Level
Formal Specifications (that is, safety and liveness
requirements for the closed loop system) returns
correct-by-construction control software that has a Worst
Case Execution Time (WCET) linear in the number of AD bits
and meets the given specifications.
We show feasibility of our approach by presenting
experimental results on using it to synthesize control
software for a buck DC-DC converter, a widely used
mixed-mode analog circuit, and for the inverted pendulum
Computational models of myocardial endomysial collagen arrangement
No full textCollagen extracellular matrix is one of the factors related to high passive stiffness of cardiac muscle. However, the architecture and the mechanical aspects of the cardiac collagen matrix are not completely known. In particular, endomysial collagen contribution to the passive mechanics of cardiac muscle as well as its micro anatomical arrangement is still a matter of debate. In order to investigate mechanical and structural properties of endomysial collagen, we consider two alternative computational models of some specific aspects of the cardiac muscle. These two models represent two different views of endomysial collagen distribution: (1) the traditional view and (2) a new view suggested by the data obtained from scanning electron microscopy (SEM) in NaOH macerated samples (a method for isolating collagen from the other tissue). We model the myocardial tissue as a net of spring elements representing the cardiomyocytes together with the endomysial collagen distribution. Each element is a viscous elastic spring, characterized by an elastic and a viscous constant. We connect these springs to imitate the interconnections between collagen fibers. Then we apply to the net of springs some external forces of suitable magnitude and direction, obtaining an extension of the net itself. In our setting, the ratio forces magnitude/net extension is intended to model the stress/strain ratio of a microscopical portion of the myocardial tissue. To solve the problem of the correct identification of the values of the different parameters involved, we use an artificial neural network approach. In particular, we use this technique to learn, given a distribution of external forces, the elastic constants of the springs needed to obtain a desired extension as an equilibrium position. Our experimental findings show that, in the model of collagen distribution structured according to the new view, a given stress/strain ratio (of the net of springs, in the sense specified above) is obtained with much smaller (w.r.t. the other model, corresponding to the traditional view) elasticity constants of the springs. This seems to indicate that by an appropriate structure, a given stiffness of the myocardial tissue can be obtained with endomysial collagen fibers of much smaller size. (c) 2007 Elsevier Ireland Ltd. All rights reserved
A multi-hop advertising discovery and delivering protocol for multi administrative domain MANET
No full textA Mobile Ad-hoc NETwork (MANET) is Multi Administrative Domain (MAD) if each network node belongs to an independent authority, that is each node owns its resources and there is no central authority owning all network nodes. One of the main obstructions in designing Service Advertising, Discovery and Delivery (SADD) protocol for MAD MANETs is the fact that, in an attempt to increase their own visibility, network nodes tend to flood the network with their advertisements. In this paper, we present a SADD protocol for MAD MANET, based on Bloom filters, that effectively prevents advertising floods due to such misbehaving nodes. Our results with the ns-2 simulator show that our SADD protocol is effective in counteracting advertising floods, it keeps low the collision rate as well as the energy consumption while ensuring that each peer receives all messages broadcasted by other peers
From Boolean Relations to Control Software
No full textAbstract—Many software as well digital hardware automatic synthesis methods define the set of implementations meeting the given system specifications with a boolean relation K. In such a context a fundamental step in the software (hardware) synthesis process is finding effective solutions to the functional equation defined by K. This entails finding a (set of) boolean function(s) F (typically represented using OBDDs, Ordered Binary Decision Diagrams) such that: 1) for all x for which K is satisfiable, K(x, F (x)) = 1 holds; 2) the implementation of F is efficient with respect to given implementation parameters such as code size or execution time. While this problem has been widely studied in digital hardware synthesis, little has been done in a software synthesis context. Unfortunately the approaches developed for hardware synthesis cannot be directly used in a software context. This motivates investigation of effective methods to solve the above problem when F has to be implemented with software. In this paper, we present an algorithm that, from an OBDD representation for K, generates a C code implementation for F that has the same size as the OBDD for F and a worst case execution time linear in nr, being n = |x | the number of input arguments for functions in F and r the number of functions in F
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
- …
