| Records |
| Author |
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 |
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 |
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 |
Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico; Venturini Zilli, Marisa |
| Title |
Finite horizon analysis of Markov Chains with the Mur$\varphi$ verifier |
Type |
Journal Article |
| Year |
2006 |
Publication |
Int. J. Softw. Tools Technol. Transf. |
Abbreviated Journal |
|
| Volume |
8 |
Issue |
4 |
Pages |
397-409 |
| Keywords |
|
| Abstract |
In this paper we present an explicit disk-based verification algorithm for Probabilistic Systems defining discrete time/finite state Markov Chains. Given a Markov Chain and an integer k (horizon), our algorithm checks whether the probability of reaching an error state in at most k steps is below a given threshold. We present an implementation of our algorithm within a suitable extension of the Mur$\varphi$ verifier. We call the resulting probabilistic model checker FHP-Mur$\varphi$ (Finite Horizon Probabilistic Mur$\varphi$). We present experimental results comparing FHP-Mur$\varphi$ with (a finite horizon subset of) PRISM, a state-of-the-art symbolic model checker for Markov Chains. Our experimental results show that FHP-Mur$\varphi$ can handle systems that are out of reach for PRISM, namely those involving arithmetic operations on the state variables (e.g. hybrid systems). |
| Address |
|
| Corporate Author |
|
Thesis |
|
| Publisher |
Springer-Verlag |
Place of Publication |
Berlin, Heidelberg |
Editor |
|
| Language |
|
Summary Language |
|
Original Title |
|
| Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
| Series Volume |
|
Series Issue |
|
Edition |
|
| ISSN |
1433-2779 |
ISBN |
|
Medium |
|
| Area |
|
Expedition |
|
Conference |
|
| Notes |
|
Approved |
yes |
| Call Number |
Sapienza @ mari @ Dimtz06 |
Serial |
78 |
| Permanent link to this record |
| |
|
| |
| Author |
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 |
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 |
Mancini, Toni; Mari, Federico; Massini, Annalisa; Melatti, Igor; Merli, Fabio; Tronci, Enrico |
| Title |
System Level Formal Verification via Model Checking Driven Simulation |
Type |
Conference Article |
| Year |
2013 |
Publication |
Proceedings of the 25th International Conference on Computer Aided Verification. July 13-19, 2013, Saint Petersburg, Russia |
Abbreviated Journal |
CAV 2013 |
| Volume |
|
Issue |
|
Pages |
296-312 |
| Keywords |
|
| Abstract |
|
| Address |
|
| Corporate Author |
|
Thesis |
|
| Publisher |
Springer - Verlag |
Place of Publication |
|
Editor |
|
| Language |
|
Summary Language |
|
Original Title |
|
| Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
| Series Volume |
8044 |
Series Issue |
|
Edition |
|
| ISSN |
0302-9743 |
ISBN |
978-3-642-39798-1 |
Medium |
|
| Area |
|
Expedition |
|
Conference |
|
| Notes |
|
Approved |
yes |
| Call Number |
Sapienza @ mari @ |
Serial |
113 |
| Permanent link to this record |
| |
|
| |
| Author |
Alimguzhin, Vadim; Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico |
| Title |
A Map-Reduce Parallel Approach to Automatic Synthesis of Control Software |
Type |
Conference Article |
| Year |
2013 |
Publication |
Proc. of International SPIN Symposium on Model Checking of Software (SPIN 2013) |
Abbreviated Journal |
International SPIN Symposium on Model Checking of Software |
| Volume |
|
Issue |
|
Pages |
43-60 |
| Keywords |
|
| Abstract |
|
| Address |
|
| Corporate Author |
|
Thesis |
|
| Publisher |
Springer - Verlag |
Place of Publication |
|
Editor |
|
| Language |
|
Summary Language |
|
Original Title |
|
| Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
| Series Volume |
7976 |
Series Issue |
|
Edition |
|
| ISSN |
0302-9743 |
ISBN |
978-3-642-39175-0 |
Medium |
|
| Area |
|
Expedition |
|
Conference |
|
| Notes |
|
Approved |
no |
| Call Number |
Sapienza @ melatti @ |
Serial |
112 |
| Permanent link to this record |
| |
|
| |
| Author |
Alimguzhin, Vadim; Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico |
| Title |
On-the-Fly Control Software Synthesis |
Type |
Conference Article |
| Year |
2013 |
Publication |
Proceedings of International SPIN Symposium on Model Checking of Software (SPIN 2013) |
Abbreviated Journal |
International SPIN Symposium on Model Checking of Software |
| Volume |
|
Issue |
|
Pages |
61-80 |
| Keywords |
|
| Abstract |
|
| Address |
|
| Corporate Author |
|
Thesis |
|
| Publisher |
Springer - Verlag |
Place of Publication |
|
Editor |
|
| Language |
|
Summary Language |
|
Original Title |
|
| Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
| Series Volume |
7976 |
Series Issue |
|
Edition |
|
| ISSN |
0302-9743 |
ISBN |
978-3-642-39175-0 |
Medium |
|
| Area |
|
Expedition |
|
Conference |
|
| Notes |
|
Approved |
yes |
| Call Number |
Sapienza @ melatti @ |
Serial |
111 |
| Permanent link to this record |
| |
|
| |
| Author |
Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico; Venturini Zilli, Marisa |
| Title |
Finite Horizon Analysis of Markov Chains with the Mur$\varphi$ Verifier |
Type |
Conference Article |
| Year |
2003 |
Publication |
Correct Hardware Design and Verification Methods, 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L'Aquila, Italy, October 21-24, 2003, Proceedings |
Abbreviated Journal |
|
| Volume |
|
Issue |
|
Pages |
394-409 |
| Keywords |
|
| Abstract |
In this paper we present an explicit disk based verification algorithm for Probabilistic Systems defining discrete time/finite state Markov Chains. Given a Markov Chain and an integer k (horizon), our algorithm checks whether the probability of reaching an error state in at most k steps is below a given threshold. We present an implementation of our algorithm within a suitable extension of the Mur$\varphi$ verifier. We call the resulting probabilistic model checker FHP-Mur$\varphi$ (Finite Horizon Probabilistic Mur$\varphi$). We present experimental results comparing FHP-Mur$\varphi$ with (a finite horizon subset of) PRISM, a state-of-the-art symbolic model checker for Markov Chains. Our experimental results show that FHP-Mur$\varphi$ can handle systems that are out of reach for PRISM, namely those involving arithmetic operations on the state variables (e.g. hybrid systems). |
| Address |
|
| Corporate Author |
|
Thesis |
|
| Publisher |
Springer |
Place of Publication |
|
Editor |
Geist, D.; Tronci, E. |
| Language |
|
Summary Language |
|
Original Title |
|
| Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
| Series Volume |
2860 |
Series Issue |
|
Edition |
|
| ISSN |
3-540-20363-X |
ISBN |
|
Medium |
|
| Area |
|
Expedition |
|
Conference |
|
| Notes |
|
Approved |
yes |
| Call Number |
Sapienza @ mari @ Dimtz03 |
Serial |
84 |
| Permanent link to this record |
