|
|
Giuseppe Della Penna, Benedetto Intrigila, Enrico Tronci, and Marisa Venturini Zilli. "Exploiting Transition Locality in the Disk Based Mur$\varphi$ Verifier." In 4th International Conference on Formal Methods in Computer-Aided Design (FMCAD), edited by M. Aagaard and J. W. O'Leary, 202–219. Lecture Notes in Computer Science 2517. Portland, OR, USA: Springer, 2002. ISSN: 3-540-00116-6. DOI: 10.1007/3-540-36126-X_13.
Abstract: The main obstruction to automatic verification of Finite State Systems is the huge amount of memory required to complete the verification task (state explosion). This motivates research on distributed as well as disk based verification algorithms. In this paper we present a disk based Breadth First Explicit State Space Exploration algorithm as well as an implementation of it within the Mur$\varphi$ verifier. Our algorithm exploits transition locality (i.e. the statistical fact that most transitions lead to unvisited states or to recently visited states) to decrease disk read accesses thus reducing the time overhead due to disk usage. A disk based verification algorithm for Mur$\varphi$ has been already proposed in the literature. To measure the time speed up due to locality exploitation we compared our algorithm with such previously proposed algorithm. Our experimental results show that our disk based verification algorithm is typically more than 10 times faster than such previously proposed disk based verification algorithm. To measure the time overhead due to disk usage we compared our algorithm with RAM based verification using the (standard) Mur$\varphi$ verifier with enough memory to complete the verification task. Our experimental results show that even when using 1/10 of the RAM needed to complete verification, our disk based algorithm is only between 1.4 and 5.3 times (3 times on average) slower than (RAM) Mur$\varphi$ with enough RAM memory to complete the verification task at hand. Using our disk based Mur$\varphi$ we were able to complete verification of a protocol with about $10^9$ reachable states. This would require more than 5 gigabytes of RAM using RAM based Mur$\varphi$.
|
|
|
|
Giuseppe Della Penna, Benedetto Intrigila, Igor Melatti, Enrico Tronci, and Marisa Venturini Zilli. "Finite horizon analysis of Markov Chains with the Mur$\varphi$ verifier." Int. J. Softw. Tools Technol. Transf. 8, no. 4 (2006): 397–409. Springer-Verlag. ISSN: 1433-2779. DOI: 10.1007/s10009-005-0216-7.
Abstract: In this paper we present an explicit disk-based verification algorithm for Probabilistic Systems defining discrete time/finite state Markov Chains. Given a Markov Chain and an integer k (horizon), our algorithm checks whether the probability of reaching an error state in at most k steps is below a given threshold. We present an implementation of our algorithm within a suitable extension of the Mur$\varphi$ verifier. We call the resulting probabilistic model checker FHP-Mur$\varphi$ (Finite Horizon Probabilistic Mur$\varphi$). We present experimental results comparing FHP-Mur$\varphi$ with (a finite horizon subset of) PRISM, a state-of-the-art symbolic model checker for Markov Chains. Our experimental results show that FHP-Mur$\varphi$ can handle systems that are out of reach for PRISM, namely those involving arithmetic operations on the state variables (e.g. hybrid systems).
|
|
|
|
Giuseppe Della Penna, Benedetto Intrigila, Igor Melatti, Enrico Tronci, and Marisa Venturini Zilli. "Finite Horizon Analysis of Markov Chains with the Mur$\varphi$ Verifier." In Correct Hardware Design and Verification Methods, 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L'Aquila, Italy, October 21-24, 2003, Proceedings, edited by D. Geist and E. Tronci, 394–409. Lecture Notes in Computer Science 2860. Springer, 2003. ISSN: 3-540-20363-X. DOI: 10.1007/978-3-540-39724-3_34.
Abstract: In this paper we present an explicit disk based verification algorithm for Probabilistic Systems defining discrete time/finite state Markov Chains. Given a Markov Chain and an integer k (horizon), our algorithm checks whether the probability of reaching an error state in at most k steps is below a given threshold. We present an implementation of our algorithm within a suitable extension of the Mur$\varphi$ verifier. We call the resulting probabilistic model checker FHP-Mur$\varphi$ (Finite Horizon Probabilistic Mur$\varphi$). We present experimental results comparing FHP-Mur$\varphi$ with (a finite horizon subset of) PRISM, a state-of-the-art symbolic model checker for Markov Chains. Our experimental results show that FHP-Mur$\varphi$ can handle systems that are out of reach for PRISM, namely those involving arithmetic operations on the state variables (e.g. hybrid systems).
|
|
|
|
Giuseppe Della Penna, Benedetto Intrigila, Igor Melatti, Enrico Tronci, and Marisa Venturini Zilli. "Finite Horizon Analysis of Stochastic Systems with the Mur$\varphi$ Verifier." In Theoretical Computer Science, 8th Italian Conference, ICTCS 2003, Bertinoro, Italy, October 13-15, 2003, Proceedings, edited by C. Blundo and C. Laneve, 58–71. Lecture Notes in Computer Science 2841. Springer, 2003. ISSN: 3-540-20216-1. DOI: 10.1007/978-3-540-45208-9_6.
Abstract: Many reactive systems are actually Stochastic Processes. Automatic analysis of such systems is usually very difficult thus typically one simplifies the analysis task by using simulation or by working on a simplified model (e.g. a Markov Chain). We present a Finite Horizon Probabilistic Model Checking approach which essentially can handle the same class of stochastic processes of a typical simulator. This yields easy modeling of the system to be analyzed together with formal verification capabilities. Our approach is based on a suitable disk based extension of the Mur$\varphi$ verifier. Moreover we present experimental results showing effectiveness of our approach.
|
|
|
|
Amedeo Cesta, Simone Fratini, Andrea Orlandini, Alberto Finzi, and Enrico Tronci. "Flexible Plan Verification: Feasibility Results." Fundamenta Informaticae 107, no. 2 (2011): 111–137. DOI: 10.3233/FI-2011-397.
|
|
|
|
Amedeo Cesta, Alberto Finzi, Simone Fratini, Andrea Orlandini, and Enrico Tronci. "Flexible Plan Verification: Feasibility Results." In 16th RCRA International Workshop on “Experimental evaluation of algorithms for solving problems with combinatorial explosion” (RCRA). Proceedings., 2009.
|
|
|
|
Amedeo Cesta, Alberto Finzi, Simone Fratini, Andrea Orlandini, and Enrico Tronci. "Flexible Timeline-Based Plan Verification." In KI 2009: Advances in Artificial Intelligence, 32nd Annual German Conference on AI, Paderborn, Germany, September 15-18, 2009. Proceedings, edited by B. Ã. ¤rbel Mertsching, M. Hund and M. Z. Aziz, 49–56. Lecture Notes in Computer Science 5803. Springer, 2009. ISSN: 978-3-642-04616-2. DOI: 10.1007/978-3-642-04617-9_7.
|
|
|
|
Marco Gribaudo, Andras Horváth, Andrea Bobbio, Enrico Tronci, Ester Ciancamerla, and Michele Minichino. "Fluid Petri Nets and hybrid model checking: a comparative case study." Int. Journal on: Reliability Engineering & System Safety 81, no. 3 (2003): 239–257. Elsevier. DOI: 10.1016/S0951-8320(03)00089-9.
Abstract: The modeling and analysis of hybrid systems is a recent and challenging research area which is actually dominated by two main lines: a functional analysis based on the description of the system in terms of discrete state (hybrid) automata (whose goal is to ascertain conformity and reachability properties), and a stochastic analysis (whose aim is to provide performance and dependability measures). This paper investigates a unifying view between formal methods and stochastic methods by proposing an analysis methodology of hybrid systems based on Fluid Petri Nets (FPNs). FPNs can be analyzed directly using appropriate tools. Our paper shows that the same FPN model can be fed to different functional analyzers for model checking. In order to extensively explore the capability of the technique, we have converted the original FPN into languages for discrete as well as hybrid as well as stochastic model checkers. In this way, a first comparison among the modeling power of well known tools can be carried out. Our approach is illustrated by means of a ’real world’ hybrid system: the temperature control system of a co-generative plant.
|
|
|
|
Riccardo Focardi, Roberto Gorrieri, Ruggero Lanotte, Andrea Maggiolo-Schettini, Fabio Martinelli, Simone Tini, and Enrico Tronci. "Formal Models of Timing Attacks on Web Privacy." Electronic Notes in Theoretical Computer Science 62 (2002): 229–243. Notes: TOSCA 2001, Theory of Concurrency, Higher Order Languages and Types. DOI: 10.1016/S1571-0661(04)00329-9.
Abstract: We model a timing attack on web privacy proposed by Felten and Schneider by using three different approaches: HL-Timed Automata, SMV model checker, and tSPA Process Algebra. Some comparative analysis on the three approaches is derived.
|
|
|
|
Silvia Mazzini, Stefano Puri, Federico Mari, Igor Melatti, and Enrico Tronci. "Formal Verification at System Level." In In: DAta Systems In Aerospace (DASIA), Org. EuroSpace, Canadian Space Agency, CNES, ESA, EUMETSAT. Instanbul, Turkey, EuroSpace., 2009.
Abstract: System 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.
|
|
