|
|
Giuseppe Della Penna, Benedetto Intrigila, Daniele Magazzeni, Igor Melatti, and Enrico Tronci. "CGMurphi: Automatic synthesis of numerical controllers for nonlinear hybrid systems." European Journal of Control 19, no. 1 (2013): 14–36. Elsevier North-Holland, Inc.. ISSN: 0947-3580. DOI: 10.1016/j.ejcon.2013.02.001.
|
|
|
|
Federico Mari, Igor Melatti, Ivano Salvo, and Enrico Tronci. "Linear Constraints and Guarded Predicates as a Modeling Language for Discrete Time Hybrid Systems." International Journal on Advances in Software vol. 6, nr 1&2 (2013): 155–169. IARIA. ISSN: 1942-2628.
Abstract: Model 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.
Keywords: Model-based software design; Linear predicates; Hybrid systems
|
|
|
|
Verzino Giovanni, Federico Cavaliere, Federico Mari, Igor Melatti, Giovanni Minei, Ivano Salvo, Yuri Yushtein, and Enrico Tronci. "Model checking driven simulation of sat procedures." In Proceedings of 12th International Conference on Space Operations (SpaceOps 2012)., 2012. DOI: 10.2514/6.2012-1275611.
|
|
|
|
Toni Mancini, Federico Mari, Annalisa Massini, Igor Melatti, and Enrico Tronci. "System Level Formal Verification via Distributed Multi-Core Hardware in the Loop Simulation." In Proc. of the 22nd Euromicro International Conference on Parallel, Distributed and Network-Based Processing. IEEE Computer Society, 2014. DOI: 10.1109/PDP.2014.32.
|
|
|
|
E. Tronci, T. Mancini, F. Mari, I. Melatti, I. Salvo, M. Prodanovic, J. K. Gruber, B. Hayes, and L. Elmegaard. "Demand-Aware Price Policy Synthesis and Verification Services for Smart Grids." In Proceedings of Smart Grid Communications (SmartGridComm), 2014 IEEE International Conference On., 2014. DOI: 10.1109/SmartGridComm.2014.7007745.
|
|
|
|
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.
|
|
|
|
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.
|
|
|
|
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.
|
|
|
|
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. "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.
|
|
