MCLab Group List of Papers -- Query Results

	MCLab Group List of Papers Home \| Show All \| Simple Search \| Advanced Search	Login Quick Search: Field: contains: ...
	11–20 of 70 records found matching your query (RSS):

Search & Display Options

Select All Deselect All

<< 1 2 3 4 5 6 7 >>

List View

Citations

Details

	Records
	Author	Alimguzhin, V.; Mari, F.; Melatti, I.; Salvo, I.; Tronci, E.
	Title	Linearising Discrete Time Hybrid Systems			Type	Journal Article
	Year	2017	Publication	IEEE Transactions on Automatic Control	Abbreviated Journal
	Volume	62	Issue	10	Pages	5357-5364
	Keywords
	Abstract	Model Based Design approaches for embedded systems aim at generating correct-by-construction control software, guaranteeing that the closed loop system (controller and plant) meets given system level formal specifications. This technical note addresses control synthesis for safety and reachability properties of possibly non-linear discrete time hybrid systems. By means of syntactical transformations that require non-linear terms to be Lipschitz continuous functions, we over-approximate non-linear dynamics with a linear system whose controllers are guaranteed to be controllers of the original system. We evaluate performance of our approach on meaningful control synthesis benchmarks, also comparing it to a state-of-the-art tool.
	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	0018-9286	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	no
	Call Number	Sapienza @ mari @ ref7902199			Serial	164
Permanent link to this record



	Author	Della Penna, Giuseppe; Di Marco, Antinisca; Intrigila, Benedetto; Melatti, Igor; Pierantonio, Alfonso
	Title	Interoperability mapping from XML schemas to ER diagrams			Type	Journal Article
	Year	2006	Publication	Data Knowl. Eng.	Abbreviated Journal
	Volume	59	Issue	1	Pages	166-188
	Keywords
	Abstract	The eXtensible Markup Language (XML) is a de facto standard on the Internet and is now being used to exchange a variety of data structures. This leads to the problem of efficiently storing, querying and retrieving a great amount of data contained in XML documents. Unfortunately, XML data often need to coexist with historical data. At present, the best solution for storing XML into pre-existing data structures is to extract the information from the XML documents and adapt it to the data structuresÃ¢â‚¬â„¢ logical model (e.g., the relational model of a DBMS). In this paper, we introduce a technique called Xere (XML entityÃ‚â€“relationship exchange) to assist the integration of XML data with other data sources. To this aim, we present an algorithm that maps XML schemas into entityÃ‚â€“relationship diagrams, discuss its soundness and completeness and show its implementation in XSLT.
	Address
	Corporate Author				Thesis
	Publisher	Elsevier Science Publishers B. V.	Place of Publication	Amsterdam, The Netherlands, The Netherlands	Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN	0169-023x	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ Ddimp06			Serial	77
Permanent link to this record



	Author	Mancini, T.; Mari, F.; Massini, A.; Melatti, I.; Tronci, E.
	Title	Anytime system level verification via parallel random exhaustive hardware in the loop simulation			Type	Journal Article
	Year	2016	Publication	Microprocessors and Microsystems	Abbreviated Journal
	Volume	41	Issue		Pages	12-28
	Keywords	Model Checking of Hybrid Systems; Model checking driven simulation; Hardware in the loop simulation
	Abstract	Abstract System level verification of cyber-physical systems has the goal of verifying that the whole (i.e., software + hardware) system meets the given specifications. Model checkers for hybrid systems cannot handle system level verification of actual systems. Thus, Hardware In the Loop Simulation (HILS) is currently the main workhorse for system level verification. By using model checking driven exhaustive HILS, System Level Formal Verification (SLFV) can be effectively carried out for actual systems. We present a parallel random exhaustive HILS based model checker for hybrid systems that, by simulating all operational scenarios exactly once in a uniform random order, is able to provide, at any time during the verification process, an upper bound to the probability that the System Under Verification exhibits an error in a yet-to-be-simulated scenario (Omission Probability). We show effectiveness of the proposed approach by presenting experimental results on SLFV of the Inverted Pendulum on a Cart and the Fuel Control System examples in the Simulink distribution. To the best of our knowledge, no previously published model checker can exhaustively verify hybrid systems of such a size and provide at any time an upper bound to the Omission Probability.
	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	0141-9331	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	no
	Call Number	MCLab @ davi @ Mancini201612			Serial	155
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	Journal Article
	Year	2014	Publication	ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY	Abbreviated Journal	ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY
	Volume	23	Issue	1	Pages	Article 6
	Keywords
	Abstract
	Address
	Corporate Author				Thesis
	Publisher	ACM	Place of Publication		Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN	1049-331X	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	no
	Call Number	Sapienza @ melatti @			Serial	110
Permanent link to this record



	Author	Della Penna, Giuseppe; Intrigila, Benedetto; Magazzeni, Daniele; Melatti, Igor; Tronci, Enrico
	Title	CGMurphi: Automatic synthesis of numerical controllers for nonlinear hybrid systems			Type	Journal Article
	Year	2013	Publication	European Journal of Control	Abbreviated Journal	European Journal of Control
	Volume	19	Issue	1	Pages	14-36
	Keywords
	Abstract
	Address
	Corporate Author				Thesis
	Publisher	Elsevier North-Holland, Inc.	Place of Publication		Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN	0947-3580	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	no
	Call Number	Sapienza @ melatti @			Serial	114
Permanent link to this record



	Author	Melatti, Igor; Palmer, Robert; Sawaya, Geoffrey; Yang, Yu; Kirby, Robert Mike; Gopalakrishnan, Ganesh
	Title	Parallel and distributed model checking in Eddy			Type	Journal Article
	Year	2009	Publication	Int. J. Softw. Tools Technol. Transf.	Abbreviated Journal
	Volume	11	Issue	1	Pages	13-25
	Keywords
	Abstract	Model checking of safety properties can be scaled up by pooling the CPU and memory resources of multiple computers. As compute clusters containing 100s of nodes, with each node realized using multi-core (e.g., 2) CPUs will be widespread, a model checker based on the parallel (shared memory) and distributed (message passing) paradigms will more efficiently use the hardware resources. Such a model checker can be designed by having each node employ two shared memory threads that run on the (typically) two CPUs of a node, with one thread responsible for state generation, and the other for efficient communication, including (1) performing overlapped asynchronous message passing, and (2) aggregating the states to be sent into larger chunks in order to improve communication network utilization. We present the design details of such a novel model checking architecture called Eddy. We describe the design rationale, details of how the threads interact and yield control, exchange messages, as well as detect termination. We have realized an instance of this architecture for the Murphi modeling language. Called Eddy_Murphi, we report its performance over the number of nodes as well as communication parameters such as those controlling state aggregation. Nearly linear reduction of compute time with increasing number of nodes is observed. Our thread task partition is done in such a way that it is modular, easy to port across different modeling languages, and easy to tune across a variety of platforms.
	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 @ Mpsykg09			Serial	80
Permanent link to this record



	Author	Hayes, B. P. ; Melatti, I.; Mancini, T.; Prodanovic, M.; Tronci, E.
	Title	Residential Demand Management using Individualised Demand Aware Price Policies			Type	Journal Article
	Year	2017	Publication	IEEE Transactions On Smart Grid	Abbreviated Journal
	Volume	8	Issue	3	Pages	1284-1294
	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		ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	no
	Call Number	MCLab @ davi @			Serial	157
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	Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico; Venturini Zilli, Marisa
	Title	Exploiting Transition Locality in Automatic Verification of Finite State Concurrent Systems			Type	Journal Article
	Year	2004	Publication	Sttt	Abbreviated Journal
	Volume	6	Issue	4	Pages	320-341
	Keywords
	Abstract	In this paper we show that statistical properties of the transition graph of a system to be verified can be exploited to improve memory or time performances of verification algorithms. We show experimentally that protocols exhibit transition locality. That is, with respect to levels of a breadth-first state space exploration, state transitions tend to be between states belonging to close levels of the transition graph. We support our claim by measuring transition locality for the set of protocols included in the Mur$\varphi$ verifier distribution. We present a cache-based verification algorithm that exploits transition locality to decrease memory usage and a disk-based verification algorithm that exploits transition locality to decrease disk read accesses, thus reducing the time overhead due to disk usage. Both algorithms have been implemented within the Mur$\varphi$ verifier. Our experimental results show that our cache-based algorithm can typically save more than 40% of memory with an average time penalty of about 50% when using (Mur$\varphi$) bit compression and 100% when using bit compression and hash compaction, whereas our disk-based verification algorithm is typically more than ten times faster than a previously proposed disk-based verification algorithm and, even when using 10% of the memory needed to complete verification, it is only between 40 and 530% (300% on average) slower than (RAM) Mur$\varphi$ with enough memory to complete the verification task at hand. Using just 300 MB of memory our disk-based Mur$\varphi$ was able to complete verification of a protocol with about $10^9$ reachable states. This would require more than 5 GB of memory using standard Mur$\varphi$.
	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		ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ DIMTZ04j			Serial	91
Permanent link to this record



	Author	Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico
	Title	Linear Constraints and Guarded Predicates as a Modeling Language for Discrete Time Hybrid Systems			Type	Journal Article
	Year	2013	Publication	International Journal on Advances in Software	Abbreviated Journal	Intern. Journal on Advances in SW
	Volume	vol. 6, nr 1&2	Issue		Pages	155-169
	Keywords	Model-based software design; Linear predicates; Hybrid systems
	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.
	Address
	Corporate Author				Thesis
	Publisher	IARIA	Place of Publication		Editor	Luigi Lavazza
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN	1942-2628	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ melatti @			Serial	115
Permanent link to this record