SmartHG Project Publications -- Query Results

	SmartHG Project Publications Home \| Show All \| Simple Search \| Advanced Search	Login Quick Search: Field: contains: ...
	1-10 of 28 records found matching your query:

Search & Display Options

Select All Deselect All

<< 1 2 3 >>

List View

Citations

Details

	Records
	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
	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
	Call Number	UNIROMA1 @ davi @ Mancini201612			Serial	59
Permanent link to this record



	Author	Mancini, T.
	Title	Now or Never: negotiating efficiently with unknown counterparts			Type
	Year	2015	Publication	In proceedings of the 22nd RCRA International Workshop. Ferrara, Italy. CEUR, 2015 (Co-located with the 14th Conference of the Italian Association for Artificial Intelligence (AI*IA 2015)).	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		ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved
	Call Number	UNIROMA1 @ davi @			Serial	53
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
	Year	2013	Publication	International Journal on Advances in Software	Abbreviated Journal
	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 insoftware based control systems (e.g., embeddedsoftware) design, since in such a case systemlevel specifications are much easier to definethan the control software behavior itself. Inturn, model based design of embedded systemsrequires modeling both continuous subsystems(typically, the plant) as well as discretesubsystems (the controller). This is typicallydone using hybrid systems. Mixed Integer LinearProgramming (MILP) based abstraction techniqueshave been successfully applied to automatically synthesize correct-by-construction controlsoftware for discrete time linear hybrid systems,where plant dynamics is modeled as a linearpredicate over state, input, and next statevariables. Unfortunately, MILP solvers requiresuch linear predicates to be conjunctions oflinear constraints, which is not a natural way ofmodeling hybrid systems. In this paper we showthat, under the hypothesis that each variableranges over a bounded interval, any linearpredicate built upon conjunction and disjunction of linear constraints can be automaticallytranslated into an equivalent conjunctivepredicate. Since variable bounds play a key rolein this translation, our algorithm includes aprocedure to compute all implicit variable boundsof the given linear predicate. Furthermore, weshow that a particular form of linear predicates,namely guarded predicates, are a natural andpowerful language to succinctly model discretetime linear hybrid systems dynamics. Finally, weexperimentally show the feasibility of ourapproach on an important and challenging casestudy taken from the literature, namely themulti-input Buck DC-DC Converter. As an example,the guarded predicate that models (with 57constraints) a 6-inputs Buck DC-DC Converter istranslated in a conjunctive predicate (with 102linear constraints) in about 40 minutes.
	Address
	Corporate Author				Thesis
	Publisher	Iaria	Place of Publication		Editor
	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
	Call Number	UNIROMA1 @ davi @ Mari_etal2013			Serial	22
Permanent link to this record



	Author	Jacobsen, R.H.; Mikkelsen, S.A.
	Title	Infrastructure for Intelligent Automation Services in the Smart Grid			Type
	Year	2014	Publication	Wireless Personal Communications	Abbreviated Journal
	Volume	76	Issue	2	Pages	125-147
	Keywords	Home area network; Smart energy profile; Intelligent automation services; Smart grid
	Abstract
	Address
	Corporate Author				Thesis
	Publisher	Springer US	Place of Publication		Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN	0929-6212	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved
	Call Number	UNIROMA1 @ davi @ JacMik14			Serial	41
Permanent link to this record



	Author	Mancini, T.; Mari, F.; Massini, A.; Melatti, I.; Tronci, E.
	Title	Simulator Semantics for System Level Formal Verification			Type
	Year	2015	Publication	Proceedings Sixth International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2015),	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		ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved
	Call Number	UNIROMA1 @ davi @			Serial	54
Permanent link to this record



	Author	Mari, F.; Melatti, I.; Salvo, I.; Tronci, E.
	Title	Model Based Synthesis of Control Software from System Level Formal Specifications			Type
	Year	2014	Publication	Acm Transactions On Software Engineering And Methodology	Abbreviated Journal
	Volume	23	Issue	1	Pages	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
	Call Number	UNIROMA1 @ davi @ Mari_etal2014			Serial	40
Permanent link to this record



	Author	Mancini, T.; Mari, F.; Massini, A.; Melatti, I.; Tronci, E.
	Title	SyLVaaS: System Level Formal Verification as a Service			Type
	Year	2016	Publication	Fundam. Inform.	Abbreviated Journal
	Volume	149	Issue	1-2	Pages	101-132
	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
	Call Number	UNIROMA1 @ davi @ DBLP:journals/fuin/ManciniMMMT16			Serial	63
Permanent link to this record



	Author	Mancini, T.
	Title	Now or Never: Negotiating Efficiently with Unknown or Untrusted Counterparts			Type
	Year	2016	Publication	Fundam. Inform.	Abbreviated Journal
	Volume	149	Issue	1-2	Pages	61-100
	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
	Call Number	UNIROMA1 @ davi @ DBLP:journals/fuin/Mancini16			Serial	62
Permanent link to this record



	Author	Alimguzhin, Vadim; Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico
	Title	On Model Based Synthesis of Embedded Control Software			Type
	Year	2012	Publication	International Conference on Embedded Software, EMSOFT	Abbreviated Journal
	Volume		Issue		Pages
	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		ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved
	Call Number	UNIROMA1 @ mari @ Alimguzhin_etal2012_2			Serial	14
Permanent link to this record



	Author	Hayes, B. P.; Gruber, J. K.; Prodanovic, M.
	Title	A closed-loop state estimation tool for MV network monitoring and operation			Type
	Year	2015	Publication	IEEE Transactions on Smart Grid	Abbreviated Journal
	Volume	PP	Issue	99	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		ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved
	Call Number	UNIROMA1 @ davi @			Serial	50
Permanent link to this record