|
|
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.
|
|
|
|
Enrico Tronci. "Formally Modeling a Metal Processing Plant and its Closed Loop Specifications." In 4th IEEE International Symposium on High-Assurance Systems Engineering (HASE), 151. Washington, D.C, USA: IEEE Computer Society, 1999. ISSN: 0-7695-0418-3. DOI: 10.1109/HASE.1999.809490.
Abstract: We present a case study on automatic synthesis of control software from formal specifications for an industrial automation control system. Our aim is to compare the effectiveness (i.e. design effort and controller quality) of automatic controller synthesis from closed loop formal specifications with that of manual controller design followed by automatic verification. The system to be controlled (plant) models a metal processing facility near Karlsruhe. We succeeded in automatically generating C code implementing a (correct by construction) embedded controller for such a plant from closed loop formal specifications. Our experimental results show that for industrial automation control systems automatic synthesis is a viable and profitable (especially as far as design effort is concerned) alternative to manual design followed by automatic verification.
|
|
|
|
Federico Mari, Igor Melatti, Ivano Salvo, and Enrico Tronci. From Boolean Functional Equations to Control Software. Vol. abs/1106.0468. CoRR, Technical Report, 2011. http://arxiv.org/abs/1106.0468 (accessed May 9, 2024).
Abstract: 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 WCET (Worst Case Execution Time) at most O(nr), being n = |x| the number of arguments of functions in F and r the number of functions in F.
|
|
|
|
Federico Mari, Igor Melatti, Ivano Salvo, and Enrico Tronci. "From Boolean Relations to Control Software." In Proceedings of ICSEA 2011, The Sixth International Conference on Software Engineering Advances, 528–533. ThinkMind, 2011. ISSN: 978-1-61208-165-6. Notes: Best Paper Award.
Abstract: 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 WCET (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.
|
|
|
|
Andrea Bobbio, Ester Ciancamerla, Michele Minichino, and Enrico Tronci. "Functional analysis of a telecontrol system and stochastic measures of its GSM/GPRS connections." Archives of Transport – International Journal of Transport Problems 17, no. 3-4 (2005).
|
|
