MCLab Group List of Papers -- Query Results

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

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	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	Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico
	Title	Quantized Feedback Control Software Synthesis from System Level Formal Specifications for Buck DC/DC Converters			Type	Report
	Year	2011	Publication		Abbreviated Journal
	Volume	abs/1105.5640	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 automatic synthesis of SBCS control software. In previous works we presented an algorithm, along with a tool QKS implementing it, that from a formal model (as a Discrete Time Linear Hybrid System, DTLHS) 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. In this technical report we present full experimental results on using it to synthesize control software for two versions of buck DC-DC converters (single-input and multi-input), a widely used mixed-mode analog circuit.
	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	106
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	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	Automatic Control Software Synthesis for Quantized Discrete Time Hybrid Systems			Type	Report
	Year	2012	Publication		Abbreviated Journal
	Volume	abs/1207.4098	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. This paper addresses control software synthesis for discrete time nonlinear systems. We present a methodology to overapproximate the dynamics of a discrete time nonlinear hybrid system H by means of a discrete time linear hybrid system L(H), in such a way that controllers for L(H) are guaranteed to be controllers for H. We present experimental results on the inverted pendulum, a challenging and meaningful benchmark in nonlinear Hybrid Systems control.
	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	103
Permanent link to this record



	Author	Mari, Federico; Tronci, Enrico
	Title	CEGAR Based Bounded Model Checking of Discrete Time Hybrid Systems			Type	Conference Article
	Year	2007	Publication	Hybrid Systems: Computation and Control (HSCC 2007)	Abbreviated Journal
	Volume		Issue		Pages	399-412
	Keywords	Model Checking, Abstraction, CEGAR, SAT, Hybrid Systems, DTHS
	Abstract	Many hybrid systems can be conveniently modeled as Piecewise Affine Discrete Time Hybrid Systems PA-DTHS. As well known Bounded Model Checking (BMC) for such systems comes down to solve a Mixed Integer Linear Programming (MILP) feasibility problem. We present a SAT based BMC algorithm for automatic verification of PA-DTHSs. Using Counterexample Guided Abstraction Refinement (CEGAR) our algorithm gradually transforms a PA-DTHS verification problem into larger and larger SAT problems. Our experimental results show that our approach can handle PA-DTHSs that are more then 50 times larger than those that can be handled using a MILP solver.
	Address
	Corporate Author				Thesis
	Publisher	Springer	Place of Publication		Editor	Bemporad, A.; Bicchi, A.; Buttazzo, G.C.
	Language		Summary Language		Original Title
	Series Editor		Series Title	Lecture Notes in Computer Science	Abbreviated Series Title
	Series Volume	4416	Series Issue		Edition
	ISSN		ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ MarTro07			Serial	92
Permanent link to this record



	Author	Piperno, Adolfo; Tronci, Enrico
	Title	Regular Systems of Equations in λ-calculus			Type	Journal Article
	Year	1990	Publication	Int. J. Found. Comput. Sci.	Abbreviated Journal
	Volume	1	Issue	3	Pages	325-340
	Keywords
	Abstract	Many problems arising in equational theories like Lambda-calculus and Combinatory Logic can be expressed by combinatory equations or systems of equations. However, the solvability problem for an arbitrarily given class of systems is in general undecidable. In this paper we shall focus our attention on a decidable class of systems, which will be called regular systems, and we shall analyse some classical problems and well-known properties of Lambda-calculus that can be described and solved by means of regular systems. The significance of such class will be emphasized showing that for slight extensions of it the solvability problem turns out to be undecidable.
	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 @ ijfcs90			Serial	60
Permanent link to this record



	Author	Piperno, Adolfo; Tronci, Enrico
	Title	Regular Systems of Equations in λ-calculus			Type	Conference Article
	Year	1989	Publication	Ictcs	Abbreviated Journal
	Volume		Issue		Pages
	Keywords
	Abstract	Many problems arising in equational theories like Lambda-calculus and Combinatory Logic can be expressed by combinatory equations or systems of equations. However, the solvability problem for an arbitrarily given class of systems is in general undecidable. In this paper we shall focus our attention on a decidable class of systems, which will be called regular systems, and we shall analyse some classical problems and well-known properties of Lambda-calculus that can be described and solved by means of regular systems. The significance of such class will be emphasized showing that for slight extensions of it the solvability problem turns out to be undecidable.
	Address
	Corporate Author				Thesis
	Publisher		Place of Publication	Mantova - Italy	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 @ ictcs89			Serial	61
Permanent link to this record



	Author	Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico; Venturini Zilli, Marisa
	Title	Finite Horizon Analysis of Stochastic Systems with the Mur$\varphi$ Verifier			Type	Conference Article
	Year	2003	Publication	Theoretical Computer Science, 8th Italian Conference, ICTCS 2003, Bertinoro, Italy, October 13-15, 2003, Proceedings	Abbreviated Journal
	Volume		Issue		Pages	58-71
	Keywords
	Abstract	Many reactive systems are actually Stochastic Processes. Automatic analysis of such systems is usually very difficult thus typically one simplifies the analysis task by using simulation or by working on a simplified model (e.g. a Markov Chain). We present a Finite Horizon Probabilistic Model Checking approach which essentially can handle the same class of stochastic processes of a typical simulator. This yields easy modeling of the system to be analyzed together with formal verification capabilities. Our approach is based on a suitable disk based extension of the Mur$\varphi$ verifier. Moreover we present experimental results showing effectiveness of our approach.
	Address
	Corporate Author				Thesis
	Publisher	Springer	Place of Publication		Editor	Blundo, C.; Laneve, C.
	Language		Summary Language		Original Title
	Series Editor		Series Title	Lecture Notes in Computer Science	Abbreviated Series Title
	Series Volume	2841	Series Issue		Edition
	ISSN	3-540-20216-1	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ DIMTZ03c			Serial	90
Permanent link to this record



	Author	Tronci, Enrico
	Title	Automatic Synthesis of Controllers from Formal Specifications			Type	Conference Article
	Year	1998	Publication	Proc of 2nd IEEE International Conference on Formal Engineering Methods (ICFEM)	Abbreviated Journal
	Volume		Issue		Pages	134-143
	Keywords
	Abstract	Many safety critical reactive systems are indeed embedded control systems. Usually a control system can be partitioned into two main subsystems: a controller and a plant. Roughly speaking: the controller observes the state of the plant and sends commands (stimulus) to the plant to achieve predefined goals. We show that when the plant can be modeled as a deterministic finite state system (FSS) it is possible to effectively use formal methods to automatically synthesize the program implementing the controller from the plant model and the given formal specifications for the closed loop system (plant+controller). This guarantees that the controller program is correct by construction. To the best of our knowledge there is no previously published effective algorithm to extract executable code for the controller from closed loop formal specifications. We show practical usefulness of our techniques by giving experimental results on their use to synthesize C programs implementing optimal controllers (OCs) for plants with more than 109 states.
	Address
	Corporate Author				Thesis
	Publisher		Place of Publication	Brisbane, Queensland, Australia	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 @ icfem98			Serial	52
Permanent link to this record