|
|
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.
|
|
|
|
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.
|
|
|
|
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
|
|
|
|
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.
|
|
|
|
Toni Mancini, Federico Mari, Annalisa Massini, Igor Melatti, Fabio Merli, and Enrico Tronci. "System Level Formal Verification via Model Checking Driven Simulation." In Proceedings of the 25th International Conference on Computer Aided Verification. July 13-19, 2013, Saint Petersburg, Russia, 296–312. Lecture Notes in Computer Science 8044. Springer - Verlag, 2013. ISSN: 0302-9743. ISBN: 978-3-642-39798-1. DOI: 10.1007/978-3-642-39799-8_21.
|
|
|
|
Vadim Alimguzhin, Federico Mari, Igor Melatti, Ivano Salvo, and Enrico Tronci. "A Map-Reduce Parallel Approach to Automatic Synthesis of Control Software." In Proc. of International SPIN Symposium on Model Checking of Software (SPIN 2013), 43–60. Lecture Notes in Computer Science 7976. Springer - Verlag, 2013. ISSN: 0302-9743. ISBN: 978-3-642-39175-0. DOI: 10.1007/978-3-642-39176-7_4.
|
|
|
|
Vadim Alimguzhin, Federico Mari, Igor Melatti, Ivano Salvo, and Enrico Tronci. "On-the-Fly Control Software Synthesis." In Proceedings of International SPIN Symposium on Model Checking of Software (SPIN 2013), 61–80. Lecture Notes in Computer Science 7976. Springer - Verlag, 2013. ISSN: 0302-9743. ISBN: 978-3-642-39175-0. DOI: 10.1007/978-3-642-39176-7_5.
|
|
|
|
Federico Mari, Igor Melatti, Ivano Salvo, and Enrico Tronci. "Model Based Synthesis of Control Software from System Level Formal Specifications." ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY 23, no. 1 (2014): Article 6. ACM. ISSN: 1049-331X. DOI: 10.1145/2559934.
|
|
|
|
Federico Mari, Igor Melatti, Enrico Tronci, and Alberto Finzi. "A multi-hop advertising discovery and delivering protocol for multi administrative domain MANET." Mobile Information Systems 3, no. 9 (2013): 261–280. IOS Press. ISSN: 1574-017x (Print) 1875-905X (Online). DOI: 10.3233/MIS-130162.
|
|
|
|
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
|
|
