liu.seSearch for publications in DiVA
Change search
ReferencesLink to record
Permanent link

Direct link
On Verification of Switched Systems using Abstractions
Linköping University, Department of Electrical Engineering, Automatic Control. Linköping University, The Institute of Technology.
1998 (English)Licentiate thesis, monograph (Other academic)
Abstract [en]

This thesis deals with modeling and analysis of a special class of hybrid systems, i.e., systems displaying behavior of both continuous and discrete nature.

We focus on the class of systems which are naturally modeled as having continuous trajectories, but where the trajectories evolve according to a system of first order differential equations with piecewise continuous right hand side. We further restrict our attention to models where the right hand side is piecewise affine in the continuous state variables. Systems which are naturally modeled in this fashion are called piecewise affine switched systems.

The modeling is packaged into a modeling framework where we take a logical approach to writing down the right hand side of the differential equations. The equations then run in combination with a finite state machine, and their interaction is specified via an interface. This framework allows a compact description of a potentially large number of affine models, as well as a modular approach to modeling of complex systems.

The analysis consists of verifying if a switched system fulfills specifications given either in terms of sets of good or bad discrete states, or as formulas in temporal logic specifying desired or undesired behavior. This kind of analysis is often applied to purely discrete systems, we therefore take the approach to discretize the switched system using conservative approximations. This is done using an automated procedure devised in this thesis. The discretization results in two different approximations, named acceptor and exceptor, which together can be utilized to obtain bounds on behavior which can be certified. We also introduce a discrete device, called reflector, which allows us to reduce the non-determinism resulting from the approximations. Furthermore, implementations of the procedure suggested, using either linear programming or quantifier elimination as computational tools, are discussed.

Together, the discrete approximations, obtained automatically from a model of a switched system, can be used to verify properties of interest. This is illustrated as we apply our methods to two relatively large examples, a chemical reactor model and a model of the landing gear of a fighter aircraft.

Place, publisher, year, edition, pages
Linköping: Linköping University Electronic Press, 1998. , 98 p.
Linköping Studies in Science and Technology. Thesis, ISSN 0280-7971 ; 705
National Category
Control Engineering
URN: urn:nbn:se:liu:diva-98126Local ID: LiU-TEK-LIC-1998:40ISBN: 91-7219-248-8 (print)OAI: diva2:652203
Available from: 2013-09-30 Created: 2013-09-30 Last updated: 2013-09-30Bibliographically approved

Open Access in DiVA

No full text

By organisation
Automatic ControlThe Institute of Technology
Control Engineering

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 38 hits
ReferencesLink to record
Permanent link

Direct link