Ester Ciancamerla, Michele Minichino, Stefano Serro, and Enrico Tronci. "Automatic Timeliness Verification of a Public Mobile Network." In 22nd International Conference on Computer Safety, Reliability, and Security (SAFECOMP), edited by S. Anderson, M. Felici and B. Littlewood, 35–48. Lecture Notes in Computer Science 2788. Edinburgh, UK: Springer, 2003. ISSN: 978-3-540-20126-7. DOI: 10.1007/978-3-540-39878-3_4.
Abstract: This paper deals with the automatic verification of the timeliness of Public Mobile Network (PMN), consisting of Mobile Nodes (MNs) and Base Stations (BSs). We use the Mur$\varphi$ Model Checker to verify that the waiting access time of each MN, under different PMN configurations and loads, and different inter arrival times of MNs in a BS cell, is always below a preassigned threshold. Our experimental results show that Model Checking can be successfully used to generate worst case scenarios and nicely complements probabilistic methods and simulation which are typically used for performance evaluation.
|
Edoardo Campagnano, Ester Ciancamerla, Michele Minichino, and Enrico Tronci. "Automatic Analysis of a Safety Critical Tele Control System." In 24th International Conference on: Computer Safety, Reliability, and Security (SAFECOMP), edited by R. Winther, B. A. Gran and G. Dahll, 94–107. Lecture Notes in Computer Science 3688. Fredrikstad, Norway: Springer, 2005. ISSN: 3-540-29200-4. DOI: 10.1007/11563228_8.
Abstract: We show how the Mur$\varphi$ model checker can be used to automatically carry out safety analysis of a quite complex hybrid system tele-controlling vehicles traffic inside a safety critical transport infrastructure such as a long bridge or a tunnel. We present the Mur$\varphi$ model we developed towards this end as well as the experimental results we obtained by running the Mur$\varphi$ verifier on our model. Our experimental results show that the approach presented here can be used to verify safety of critical dimensioning parameters (e.g. bandwidth) of the telecommunication network embedded in a safety critical system.
|
Federico Mari, Igor Melatti, Ivano Salvo, Enrico Tronci, Lorenzo Alvisi, Allen Clement, and Harry Li. "Model Checking Coalition Nash Equilibria in MAD Distributed Systems." In Stabilization, Safety, and Security of Distributed Systems, 11th International Symposium, SSS 2009, Lyon, France, November 3-6, 2009. Proceedings, edited by R. Guerraoui and F. Petit, 531–546. Lecture Notes in Computer Science 5873. Springer, 2009. DOI: 10.1007/978-3-642-05118-0_37.
Abstract: We present two OBDD based model checking algorithms for the verification of Nash equilibria in finite state mechanisms modeling Multiple Administrative Domains (MAD) distributed systems with possibly colluding agents (coalitions) and with possibly faulty or malicious nodes (Byzantine agents). Given a finite state mechanism, a proposed protocol for each agent and the maximum sizes f for Byzantine agents and q for agents collusions, our model checkers return Pass if the proposed protocol is an ε-f-q-Nash equilibrium, i.e. no coalition of size up to q may have an interest greater than ε in deviating from the proposed protocol when up to f Byzantine agents are present, Fail otherwise. We implemented our model checking algorithms within the NuSMV model checker: the first one explicitly checks equilibria for each coalition, while the second represents symbolically all coalitions. We present experimental results showing their effectiveness for moderate size mechanisms. For example, we can verify coalition Nash equilibria for mechanisms which corresponding normal form games would have more than $5 \times 10^21$ entries. Moreover, we compare the two approaches, and the explicit algorithm turns out to outperform the symbolic one. To the best of our knowledge, no model checking algorithm for verification of Nash equilibria of mechanisms with coalitions has been previously published.
|
Enrico Tronci. "Introductory Paper." Sttt 8, no. 4-5 (2006): 355–358. DOI: 10.1007/s10009-005-0212-y.
Abstract: In today’s competitive market designing of digital systems (hardware as well as software) faces tremendous challenges. In fact, notwithstanding an ever decreasing project budget, time to market and product lifetime, designers are faced with an ever increasing system complexity and customer expected quality. The above situation calls for better and better formal verification techniques at all steps of the design flow. This special issue is devoted to publishing revised versions of contributions first presented at the 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME) held 21–24 October 2003 in L’Aquila, Italy. Authors of well regarded papers from CHARME’03 were invited to submit to this special issue. All papers included here have been suitably extended and have undergone an independent round of reviewing.
|
|
Enrico Tronci. "Equational Programming in Lambda-Calculus via SL-Systems. Part 1." Theoretical Computer Science 160, no. 1&2 (1996): 145–184. DOI: 10.1016/0304-3975(95)00105-0.
|
|
Enrico Tronci. "Equational Programming in Lambda-Calculus via SL-Systems. Part 2." Theoretical Computer Science 160, no. 1&2 (1996): 185–216. DOI: 10.1016/0304-3975(95)00106-9.
|
Andrea Bobbio, Sandro Bologna, Michele Minichino, Ester Ciancamerla, Piero Incalcaterra, Corrado Kropp, and Enrico Tronci. "Advanced techniques for safety analysis applied to the gas turbine control system of Icaro co generative plant." In X Convegno Tecnologie e Sistemi Energetici Complessi, 339–350. Genova, Italy, 2001.
Abstract: The paper describes two complementary and integrable approaches, a probabilistic one and a deterministic one, based on classic and advanced modelling techniques for safety analysis of complex computer based systems. The probabilistic approach is based on classical and innovative probabilistic analysis methods. The deterministic approach is based on formal verification methods. Such approaches are applied to the gas turbine control system of ICARO co generative plant, in operation at ENEA CR Casaccia. The main difference between the two approaches, behind the underlining different theories, is that the probabilistic one addresses the control system by itself, as the set of sensors, processing units and actuators, while the deterministic one also includes the behaviour of the equipment under control which interacts with the control system. The final aim of the research, documented in this paper, is to explore an innovative method which put the probabilistic and deterministic approaches in a strong relation to overcome the drawbacks of their isolated, selective and fragmented use which can lead to inconsistencies in the evaluation results.
|
Amedeo Cesta, Alberto Finzi, Simone Fratini, Andrea Orlandini, and Enrico Tronci. "Verifying Flexible Timeline-based Plans." In E-Proc. of ICAPS Workshop on Validation and Verification of Planning and Scheduling Systems., 2009.
Abstract: The synthesis of flexible temporal plans has demonstrated wide applications possibilities in heterogeneous domains. We are currently studying the connection between plan generation and execution from the particular perspective of verifying a flexible plan before actual execution. This paper explores how a model-checking verification tool, based on UPPAAL-TIGA, is suitable for verifying flexible temporal plans. We first describe the formal model, the formalism, and the verification method. Furthermore we discuss our own approach and some preliminary empirical results using a real-world case study.
|
|
Ed Kuijpers, Luigi Carotenuto, Jean- Cristophe Malapert, Daniela Markov-Vetter, Igor Melatti, Andrea Orlandini, and Ranni Pinchuk. "Collaboration on ISS Experiment Data and Knowledge Representation." In Proc. of IAC 2012. Vol. D.5.11., 2012.
|
Federico Mari, Igor Melatti, Ivano Salvo, and Enrico Tronci. "Synthesizing Control Software from Boolean Relations." International Journal on Advances in Software vol. 5, nr 3&4 (2012): 212–223. IARIA. ISSN: 1942-2628.
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 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. Moreover, a formal
proof of the proposed algorithm correctness is
also shown. Finally, we present experimental
results showing effectiveness of the proposed
algorithm.
Keywords: Control Software Synthesis; Embedded Systems; Model Checking
|
