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.
Originalsprog | Engelsk |
---|---|
Titel | 2010 IEEE Conference on Emerging Technologies and Factory Automation (ETFA) |
Antal sider | 8 |
Forlag | IEEE Press |
Publikationsdato | 2010 |
Sider | 1-8 |
ISBN (Trykt) | 978-1-4244-6848-5 |
DOI | |
Status | Udgivet - 2010 |
Begivenhed | 2010 IEEE Conference on Emerging Technologies and Factory Automation - Bilbao, Spanien Varighed: 13 sep. 2010 → 16 sep. 2010 |
Konference
Konference | 2010 IEEE Conference on Emerging Technologies and Factory Automation |
---|---|
Land/Område | Spanien |
By | Bilbao |
Periode | 13/09/2010 → 16/09/2010 |