MCLab Group List of Papers -- Query Results

	MCLab Group List of Papers Home \| Show All \| Simple Search \| Advanced Search	Login Quick Search: Field: contains: ...
	31–40 of 63 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	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	Alimguzhin, Vadim; Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico
	Title	On Model Based Synthesis of Embedded Control Software			Type	Report
	Year	2012	Publication		Abbreviated Journal
	Volume	abs/1207.4474	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 control software. Given the formal model of a plant as a Discrete Time Linear Hybrid System and the implementation specifications (that is, number of bits in the Analog-to-Digital (AD) conversion) correct-by-construction control software can be automatically generated from System Level Formal Specifications of the closed loop system (that is, safety and liveness requirements), by computing a suitable finite abstraction of the plant. With respect to given implementation specifications, the automatically generated code implements a time optimal control strategy (in terms of set-up time), has a Worst Case Execution Time linear in the number of AD bits $b$, but unfortunately, its size grows exponentially with respect to $b$. In many embedded systems, there are severe restrictions on the computational resources (such as memory or computational power) available to microcontroller devices. This paper addresses model based synthesis of control software by trading system level non-functional requirements (such us optimal set-up time, ripple) with software non-functional requirements (its footprint). Our experimental results show the effectiveness of our approach: for the inverted pendulum benchmark, by using a quantization schema with 12 bits, the size of the small controller is less than 6% of the size of the time optimal one.
	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	102
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	Report
	Year	2012	Publication		Abbreviated Journal
	Volume	abs/1210.2276	Issue		Pages
	Keywords
	Abstract	Many Control Systems are indeed Software Based Control Systems, i.e. 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 control software. Available algorithms and tools (e.g., QKS) may require weeks or even months of computation to synthesize control software for large-size systems. This motivates search for parallel algorithms for control software synthesis. In this paper, we present a map-reduce style parallel algorithm for control software synthesis when the controlled system (plant) is modeled as discrete time linear hybrid system. Furthermore we present an MPI-based implementation PQKS of our algorithm. To the best of our knowledge, this is the first parallel approach for control software synthesis. We experimentally show effectiveness of PQKS on two classical control synthesis problems: the inverted pendulum and the multi-input buck DC/DC converter. Experiments show that PQKS efficiency is above 65%. As an example, PQKS requires about 16 hours to complete the synthesis of control software for the pendulum on a cluster with 60 processors, instead of the 25 days needed by the sequential algorithm in QKS.
	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	101
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	Conference Article
	Year	2012	Publication	Proceedings of the 12th International Conference on Embedded Software, EMSOFT 2012, part of the Eighth Embedded Systems Week, ESWeek 2012, Tampere, Finland, October 7-12, 2012	Abbreviated Journal
	Volume		Issue		Pages	227-236
	Keywords
	Abstract
	Address
	Corporate Author				Thesis
	Publisher	ACM	Place of Publication		Editor	Ahmed Jerraya and Luca P. Carloni and Florence Maraninchi and John Regehr
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN		ISBN	978-1-4503-1425-1	Medium
	Area		Expedition		Conference
	Notes	Techreport version can be found at arxiv.org			Approved	yes
	Call Number	Sapienza @ mari @ emsoft12			Serial	97
Permanent link to this record



	Author	Chierichetti, Flavio; Lattanzi, Silvio; Mari, Federico; Panconesi, Alessandro
	Title	On Placing Skips Optimally in Expectation			Type	Conference Article
	Year	2008	Publication	Web Search and Web Data Mining (WSDM 2008)	Abbreviated Journal
	Volume		Issue		Pages	15-24
	Keywords	Information Retrieval
	Abstract	We study the problem of optimal skip placement in an inverted list. Assuming the query distribution to be known in advance, we formally prove that an optimal skip placement can be computed quite efficiently. Our best algorithm runs in time O(n log n), n being the length of the list. The placement is optimal in the sense that it minimizes the expected time to process a query. Our theoretical results are matched by experiments with a real corpus, showing that substantial savings can be obtained with respect to the tra- ditional skip placement strategy, that of placing consecutive skips, each spanning sqrt(n) many locations.
	Address
	Corporate Author				Thesis
	Publisher	Acm	Place of Publication		Editor	Najork, M.; Broder, A.Z.; Chakrabarti, S.
	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 @ ChiLatMar08			Serial	94
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	Mancini, Toni; Mari, Federico; Massini, Annalisa; Melatti, Igor; Tronci, Enrico
	Title	Simulator Semantics for System Level Formal Verification			Type	Conference Article
	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	no
	Call Number	MCLab @ davi @			Serial	125
Permanent link to this record



	Author	Melatti, I.; Mari, F.; Mancini, T.; Prodanovic, M.; Tronci, E.
	Title	A Two-Layer Near-Optimal Strategy for Substation Constraint Management via Home Batteries			Type	Journal Article
	Year	2021	Publication	IEEE Transactions on Industrial Electronics	Abbreviated Journal
	Volume		Issue		Pages	1-1
	Keywords
	Abstract	Within electrical distribution networks, substation constraints management requires that aggregated power demand from residential users is kept within suitable bounds. Efficiency of substation constraints management can be measured as the reduction of constraints violations w.r.t. unmanaged demand. Home batteries hold the promise of enabling efficient and user-oblivious substation constraints management. Centralized control of home batteries would achieve optimal efficiency. However, it is hardly acceptable by users, since service providers (e.g., utilities or aggregators) would directly control batteries at user premises. Unfortunately, devising efficient hierarchical control strategies, thus overcoming the above problem, is far from easy. We present a novel two-layer control strategy for home batteries that avoids direct control of home devices by the service provider and at the same time yields near-optimal substation constraints management efficiency. Our simulation results on field data from 62 households in Denmark show that the substation constraints management efficiency achieved with our approach is at least 82% of the one obtained with a theoretical optimal centralized strategy.
	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	To appear			Approved	no
	Call Number	MCLab @ davi @ ref9513535			Serial	190
Permanent link to this record



	Author	Alimguzhin, V.; Mari, F.; Melatti, I.; Tronci, E.; Ebeid, E.; Mikkelsen, S.A.; Jacobsen, R.H.; Gruber, J.K.; Hayes, B.; Huerta, F.; Prodanovic, M.
	Title	A Glimpse of SmartHG Project Test-bed and Communication Infrastructure			Type	Conference Article
	Year	2015	Publication	Digital System Design (DSD), 2015 Euromicro Conference on	Abbreviated Journal
	Volume		Issue		Pages	225-232
	Keywords	Batteries; Control systems; Databases; Production; Sensors; Servers; Smart grids; Grid State Estimation; Peak Shaving; Policy Robustness Verification; Price Policy Synthesis
	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	Sapienza @ preissler @ Alimguzhin_etal2015			Serial	127
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