MCLab Group List of Papers -- Query Results

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

Search & Display Options

Select All Deselect All

<< 1 2 3 4 5 6 7 8 9 10 >> [11–13]

List View

Citations

Details

	Records
	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	Mancini, T.; Melatti, I.; Tronci, E.
	Title	Any-horizon uniform random sampling and enumeration of constrained scenarios for simulation-based formal verification			Type	Journal Article
	Year	2021	Publication	IEEE Transactions on Software Engineering	Abbreviated Journal
	Volume		Issue		Pages	1-1
	Keywords
	Abstract	Model-based approaches to the verification of non-terminating Cyber-Physical Systems (CPSs) usually rely on numerical simulation of the System Under Verification (SUV) model under input scenarios of possibly varying duration, chosen among those satisfying given constraints. Such constraints typically stem from requirements (or assumptions) on the SUV inputs and its operational environment as well as from the enforcement of additional conditions aiming at, e.g., prioritising the (often extremely long) verification activity, by, e.g., focusing on scenarios explicitly exercising selected requirements, or avoiding </i>vacuity</i> in their satisfaction. In this setting, the possibility to efficiently sample at random (with a known distribution, e.g., uniformly) within, or to efficiently enumerate (possibly in a uniformly random order) scenarios among those satisfying all the given constraints is a key enabler for the practical viability of the verification process, e.g., via simulation-based statistical model checking. Unfortunately, in case of non-trivial combinations of constraints, iterative approaches like Markovian random walks in the space of sequences of inputs in general fail in extracting scenarios according to a given distribution (e.g., uniformly), and can be very inefficient to produce at all scenarios that are both legal (with respect to SUV assumptions) and of interest (with respect to the additional constraints). For example, in our case studies, up to 91% of the scenarios generated using such iterative approaches would need to be neglected. In this article, we show how, given a set of constraints on the input scenarios succinctly defined by multiple finite memory monitors, a data structure (scenario generator) can be synthesised, from which any-horizon scenarios satisfying the input constraints can be efficiently extracted by (possibly uniform) random sampling or (randomised) enumeration. Our approach enables seamless support to virtually all simulation-based approaches to CPS verification, ranging from simple random testing to statistical model checking and formal (i.e., exhaustive) verification, when a suitable bound on the horizon or an iterative horizon enlargement strategy is defined, as in the spirit of bounded model checking.
	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	1939-3520	ISBN		Medium
	Area		Expedition		Conference
	Notes	To appear			Approved	no
	Call Number	MCLab @ davi @ ref9527998			Serial	191
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.; 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	Mancini, T.; Mari, F.; Melatti, I.; Salvo, I.; Tronci, E.; Gruber, J.; Hayes, B.; Prodanovic, M.; Elmegaard, L.
	Title	Parallel Statistical Model Checking for Safety Verification in Smart Grids			Type	Conference Article
	Year	2018	Publication	2018 IEEE International Conference on Communications, Control, and Computing Technologies for Smart Grids (SmartGridComm)	Abbreviated Journal
	Volume		Issue		Pages	1-6
	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 @ mancini-etal:2018:smartgridcomm			Serial	170
Permanent link to this record



	Author	Tronci, E.; Mancini, T.; Mari, F.; Melatti, I.; Salvo, I.; Prodanovic, M.; Gruber, J. K.; Hayes, B.; Elmegaard, L.
	Title	Demand-Aware Price Policy Synthesis and Verification Services for Smart Grids			Type	Conference Article
	Year	2014	Publication	Proceedings of Smart Grid Communications (SmartGridComm), 2014 IEEE International Conference On	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	Sapienza @ melatti @			Serial	121
Permanent link to this record



	Author	Driouich, Y.; Parente, M.; Tronci, E.
	Title	Modeling cyber-physical systems for automatic verification			Type	Conference Article
	Year	2017	Publication	14th International Conference on Synthesis, Modeling, Analysis and Simulation Methods and Applications to Circuit Design (SMACD 2017)	Abbreviated Journal
	Volume		Issue		Pages	1-4
	Keywords	cyber-physical systems;formal verification;maximum power point trackers;power engineering computing;Modelica;automatic verification;complex power electronics systems;cyber-physical systems modeling;distributed maximum power point tracking system;open standard modeling language;Computational modeling;Control systems;Integrated circuit modeling;Mathematical model;Maximum power point trackers;Object oriented modeling;Radiation effects;Automatic Formal Verification;Cyber-Physical Systems;DMPPT;Modeling;Photovoltaic systems;Simulation;System Analysis and Design
	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 @ ref7981621			Serial	168
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		ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	no
	Call Number	MCLab @ davi @			Serial	123
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		ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	no
	Call Number	Sapienza @ melatti @			Serial	118
Permanent link to this record



	Author	Tronci, Enrico
	Title	Hardware Verification, Boolean Logic Programming, Boolean Functional Programming			Type	Conference Article
	Year	1995	Publication	Tenth Annual IEEE Symposium on Logic in Computer Science (LICS)	Abbreviated Journal
	Volume		Issue		Pages	408-418
	Keywords
	Abstract	One of the main obstacles to automatic verification of finite state systems (FSSs) is state explosion. In this respect automatic verification of an FSS M using model checking and binary decision diagrams (BDDs) has an intrinsic limitation: no automatic global optimization of the verification task is possible until a BDD representation for M is generated. This is because systems and specifications are defined using different languages. To perform global optimization before generating a BDD representation for M we propose to use the same language to define systems and specifications. We show that first order logic on a Boolean domain yields an efficient functional programming language that can be used to represent, specify and automatically verify FSSs, e.g. on a SUN Sparc Station 2 we were able to automatically verify a 64 bit commercial multiplier.
	Address
	Corporate Author				Thesis
	Publisher	IEEE Computer Society	Place of Publication	San Diego, California	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 @ lics95			Serial	56
Permanent link to this record