|   | 
Details
   web
Records
Author (up) Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico
Title Model Based Synthesis of Control Software from System Level Formal Specifications Type Report
Year 2013 Publication Abbreviated Journal
Volume abs/1107.5638 Issue Pages
Keywords
Abstract Many Embedded Systems are indeed Software Based Control Systems, that is control systems whose controller consists of control software running on a microcontroller device. This motivates investigation on Formal Model Based Design approaches for automatic synthesis of embedded systems control software.
We present an algorithm, along with a tool QKS implementing it, that from a formal model (as a Discrete Time Linear Hybrid System) of the controlled system (plant), implementation specifications (that is, number of bits in the Analog-to-Digital, AD, conversion) and System Level Formal Specifications (that is, safety and liveness requirements for the closed loop system) returns correct-by-construction control software that has a Worst Case Execution Time (WCET) linear in the number of AD bits and meets the given specifications.
We show feasibility of our approach by presenting experimental results on using it to synthesize control software for a buck DC-DC converter, a widely used mixed-mode analog circuit, and for the inverted pendulum.
Address
Corporate Author Thesis
Publisher CoRR, Technical Report Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ Serial 104
Permanent link to this record
 

 
Author (up) Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico
Title Linear Constraints as a Modeling Language for Discrete Time Hybrid Systems Type Conference Article
Year 2012 Publication Proceedings of ICSEA 2012, The Seventh International Conference on Software Engineering Advances Abbreviated Journal
Volume Issue Pages 664-671
Keywords
Abstract
Address
Corporate Author Thesis
Publisher ThinkMind Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ icsea12 Serial 98
Permanent link to this record
 

 
Author (up) Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico
Title Control Software Visualization Type Conference Article
Year 2012 Publication Proceedings of INFOCOMP 2012, The Second International Conference on Advanced Communications and Computation Abbreviated Journal
Volume Issue Pages 15-20
Keywords
Abstract
Address
Corporate Author Thesis
Publisher ThinkMind Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN 978-1-61208-226-4 ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ infocomp2012 Serial 100
Permanent link to this record
 

 
Author (up) Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico
Title Undecidability of Quantized State Feedback Control for Discrete Time Linear Hybrid Systems Type Book Chapter
Year 2012 Publication Theoretical Aspects of Computing – ICTAC 2012 Abbreviated Journal
Volume Issue Pages 243-258
Keywords
Abstract
Address
Corporate Author Thesis
Publisher Springer Berlin Heidelberg Place of Publication Editor Roychoudhury, A.; D'Souza, M.
Language Summary Language Original Title
Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title
Series Volume 7521 Series Issue Edition
ISSN ISBN 978-3-642-32942-5 Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ Mari2012 Serial 99
Permanent link to this record
 

 
Author (up) Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico
Title Quantized Feedback Control Software Synthesis from System Level Formal Specifications for Buck DC/DC Converters Type Report
Year 2011 Publication Abbreviated Journal
Volume abs/1105.5640 Issue Pages
Keywords
Abstract Many Embedded Systems are indeed Software Based Control Systems (SBCSs), that is control systems whose controller consists of control software running on a microcontroller device. This motivates investigation on Formal Model Based Design approaches for automatic synthesis of SBCS control software. In previous works we presented an algorithm, along with a tool QKS implementing it, that from a formal model (as a Discrete Time Linear Hybrid System, DTLHS) of the controlled system (plant), implementation specifications (that is, number of bits in the Analog-to-Digital, AD, conversion) and System Level Formal Specifications (that is, safety and liveness requirements for the closed loop system) returns correct-by-construction control software that has a Worst Case Execution Time (WCET) linear in the number of AD bits and meets the given specifications. In this technical report we present full experimental results on using it to synthesize control software for two versions of buck DC-DC converters (single-input and multi-input), a widely used mixed-mode analog circuit.
Address
Corporate Author Thesis
Publisher CoRR, Technical Report Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ Serial 106
Permanent link to this record
 

 
Author (up) Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico
Title From Boolean Functional Equations to Control Software Type Report
Year 2011 Publication Abbreviated Journal
Volume abs/1106.0468 Issue Pages
Keywords
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.
Address
Corporate Author Thesis
Publisher CoRR, Technical Report Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ Serial 105
Permanent link to this record
 

 
Author (up) Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico
Title From Boolean Relations to Control Software Type Conference Article
Year 2011 Publication Proceedings of ICSEA 2011, The Sixth International Conference on Software Engineering Advances Abbreviated Journal
Volume Issue Pages 528-533
Keywords
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.
Address
Corporate Author Thesis
Publisher ThinkMind Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN 978-1-61208-165-6 ISBN Medium
Area Expedition Conference
Notes Best Paper Award Approved yes
Call Number Sapienza @ mari @ icsea11 Serial 14
Permanent link to this record
 

 
Author (up) Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico
Title Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid Systems Type Conference Article
Year 2010 Publication Computer Aided Verification Abbreviated Journal
Volume Issue Pages 180-195
Keywords
Abstract We present an algorithm that given a Discrete Time Linear Hybrid System returns a correct-by-construction software implementation K for a (near time optimal) robust quantized feedback controller for along with the set of states on which K is guaranteed to work correctly (controllable region). Furthermore, K has a Worst Case Execution Time linear in the number of bits of the quantization schema.
Address
Corporate Author Thesis
Publisher Springer Berlin / Heidelberg Place of Publication Editor Touili, T.; Cook, B.; Jackson, P.
Language Summary Language Original Title
Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title
Series Volume 6174 Series Issue Edition
ISSN ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ cav2010 Serial 16
Permanent link to this record
 

 
Author (up) Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico; Alvisi, Lorenzo; Clement, Allen; Li, Harry
Title Model Checking Coalition Nash Equilibria in MAD Distributed Systems Type Conference Article
Year 2009 Publication Stabilization, Safety, and Security of Distributed Systems, 11th International Symposium, SSS 2009, Lyon, France, November 3-6, 2009. Proceedings Abbreviated Journal
Volume Issue Pages 531-546
Keywords
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.
Address
Corporate Author Thesis
Publisher Springer Place of Publication Editor Guerraoui, R.; Petit, F.
Language Summary Language Original Title
Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title
Series Volume 5873 Series Issue Edition
ISSN ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ sss09 Serial 19
Permanent link to this record
 

 
Author (up) Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico; Alvisi, Lorenzo; Clement, Allen; Li, Harry
Title Model Checking Nash Equilibria in MAD Distributed Systems Type Conference Article
Year 2008 Publication FMCAD '08: Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design Abbreviated Journal
Volume Issue Pages 1-8
Keywords Model Checking, MAD Distributed System, Nash Equilibrium
Abstract We present a symbolic model checking algorithm for verification of Nash equilibria in finite state mechanisms modeling Multiple Administrative Domains (MAD) distributed systems. Given a finite state mechanism, a proposed protocol for each agent and an indifference threshold for rewards, our model checker returns PASS if the proposed protocol is a Nash equilibrium (up to the given indifference threshold) for the given mechanism, FAIL otherwise. We implemented our model checking algorithm inside the NuSMV model checker and present experimental results showing its effectiveness for moderate size mechanisms. For example, we can handle mechanisms which corresponding normal form games would have more than $10^20$ entries. To the best of our knowledge, no model checking algorithm for verification of mechanism Nash equilibria has been previously published.
Address
Corporate Author Thesis
Publisher IEEE Press Place of Publication Piscataway, NJ, USA Editor Cimatti, A.; Jones, R.
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN 978-1-4244-2735-2 ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ MarMelSalTroAlvCle08 Serial 93
Permanent link to this record