Verification and controller synthesis for resource-constrained real-time systems: case study of an autonomous truck

Shuhao Li, Paul Pettersson

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

1 Citationer (Scopus)

Abstract

An embedded system is often subject to timing constraints, resource constraints, and it should operate properly no matter how its environment behaves. This paper proposes to use timed game automata to characterize the timed behaviors and the environment uncertainties, and use piece-wise constant integer functions to approximate the continuous resources in real-time embedded systems. Based on these formal models and techniques, we employ the realtime model checker UPPAAL to verify a system against a given functional and/or timing requirement. Furthermore, we employ the timed game solver UPPAAL-TIGA to check whether a given control objective can be enforced, and if so, we synthesize a controller for the system. We carry out a case study of this approach on a battery-powered autonomous truck. Experimental results indicate that the method is effective and computationally feasible.
OriginalsprogEngelsk
Titel2010 IEEE Conference on Emerging Technologies and Factory Automation (ETFA)
Antal sider8
ForlagIEEE Press
Publikationsdato2010
Sider1-8
ISBN (Trykt)978-1-4244-6848-5
DOI
StatusUdgivet - 2010
Begivenhed2010 IEEE Conference on Emerging Technologies and Factory Automation - Bilbao, Spanien
Varighed: 13 sep. 201016 sep. 2010

Konference

Konference2010 IEEE Conference on Emerging Technologies and Factory Automation
Land/OmrådeSpanien
ByBilbao
Periode13/09/201016/09/2010

Bibliografisk note

ISSN: 1946-0740

Citationsformater