|   | 
Details
   web
Records
Author Tronci, E.; Mancini, T.; Mari, F.; Melatti, I.; Jacobsen, R. H.; Ebeid, E.; Mikkelsen, S. A.; Prodanovic, M.; Gruber, J. K.; Hayes, B.
Title SmartHG: Energy Demand Aware Open Services for Smart Grid Intelligent Automation Type Conference Article
Year 2014 Publication Proceedings of the Work in Progress Session of SEAA/DSD 2014 Abbreviated Journal
Volume Issue Pages
Keywords
Abstract
Address
Corporate Author Thesis
Publisher Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN (up) ISBN 978-3-902457-40-0 Medium
Area Expedition Conference
Notes Approved no
Call Number Sapienza @ mari @ Serial 119
Permanent link to this record
 

 
Author Mancini, Toni ; Mari, Federico ; Massini, Annalisa; Melatti, Igor; Tronci, Enrico
Title System Level Formal Verification via Distributed Multi-Core Hardware in the Loop Simulation Type Conference Article
Year 2014 Publication Proc. of the 22nd Euromicro International Conference on Parallel, Distributed and Network-Based Processing Abbreviated Journal Euromicro International Conference on Parallel, Distributed and Network-Based Processing
Volume Issue Pages
Keywords
Abstract
Address
Corporate Author Thesis
Publisher IEEE Computer Society Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN (up) ISBN Medium
Area Expedition Conference
Notes Approved no
Call Number Sapienza @ melatti @ Serial 118
Permanent link to this record
 

 
Author Verzino Giovanni ; Cavaliere, Federico; Mari, Federico; Melatti, Igor; Minei, Giovanni; Salvo, Ivano; Yushtein, Yuri; Tronci, Enrico
Title Model checking driven simulation of sat procedures Type Conference Article
Year 2012 Publication Proceedings of 12th International Conference on Space Operations (SpaceOps 2012) Abbreviated Journal International Conference on Space Operations
Volume Issue Pages
Keywords
Abstract
Address
Corporate Author Thesis
Publisher Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN (up) ISBN Medium
Area Expedition Conference
Notes Approved no
Call Number Sapienza @ melatti @ Serial 117
Permanent link to this record
 

 
Author 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 (up) ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ Serial 106
Permanent link to this record
 

 
Author 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 (up) ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ Serial 105
Permanent link to this record
 

 
Author 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 (up) ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ Serial 104
Permanent link to this record
 

 
Author Cavaliere, Federico; Mari, Federico; Melatti, Igor; Minei, Giovanni; Salvo, Ivano; Tronci, Enrico; Verzino, Giovanni; Yushtein, Yuri
Title Model Checking Satellite Operational Procedures Type Conference Article
Year 2011 Publication DAta Systems In Aerospace (DASIA), Org. EuroSpace, Canadian Space Agency, CNES, ESA, EUMETSAT. San Anton, Malta, EuroSpace. Abbreviated Journal
Volume Issue Pages
Keywords
Abstract We present a model checking approach for the automatic verification of satellite operational procedures (OPs). Building a model for a complex system as a satellite is a hard task. We overcome this obstruction by using a suitable simulator (SIMSAT) for the satellite. Our approach aims at improving OP quality assurance by automatic exhaustive exploration of all possible simulation scenarios. Moreover, our solution decreases OP verification costs by using a model checker (CMurphi) to automatically drive the simulator. We model OPs as user-executed programs observing the simulator telemetries and sending telecommands to the simulator. In order to assess feasibility of our approach we present experimental results on a simple meaningful scenario. Our results show that we can save up to 90% of verification time.
Address
Corporate Author Thesis
Publisher Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN (up) ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ Dasia11 Serial 13
Permanent link to this record
 

 
Author Mancini, Toni; Mari, Federico; Massini, Annalisa; Melatti, Igor; Tronci, Enrico
Title Anytime System Level Verification via Random Exhaustive Hardware In The Loop Simulation Type Conference Article
Year 2014 Publication In Proceedings of 17th EuroMicro Conference on Digital System Design (DSD 2014) Abbreviated Journal
Volume Issue Pages
Keywords
Abstract
Address
Corporate Author Thesis
Publisher Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN (up) ISBN Medium
Area Expedition Conference
Notes Approved no
Call Number MCLab @ davi @ Serial 122
Permanent link to this record
 

 
Author Mancini, Toni; Mari, Federico; Massini, Annalisa; Melatti, Igor; Tronci, Enrico
Title SyLVaaS: System Level Formal Verification as a Service Type Conference Article
Year 2015 Publication Proceedings of the 23rd Euromicro International Conference on Parallel, Distributed and Network-based Processing (PDP 2015), special session on Formal Approaches to Parallel and Distributed Systems (4PAD) Abbreviated Journal
Volume Issue Pages
Keywords
Abstract
Address
Corporate Author Thesis
Publisher Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN (up) ISBN Medium
Area Expedition Conference
Notes Approved no
Call Number MCLab @ davi @ Serial 123
Permanent link to this record
 

 
Author Alimguzhin, Vadim; Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico
Title Automatic Control Software Synthesis for Quantized Discrete Time Hybrid Systems Type Report
Year 2012 Publication Abbreviated Journal
Volume abs/1207.4098 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. This paper addresses control software synthesis for discrete time nonlinear systems. We present a methodology to overapproximate the dynamics of a discrete time nonlinear hybrid system H by means of a discrete time linear hybrid system L(H), in such a way that controllers for L(H) are guaranteed to be controllers for H. We present experimental results on the inverted pendulum, a challenging and meaningful benchmark in nonlinear Hybrid Systems control.
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 (up) ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ Serial 103
Permanent link to this record