Embedded systems must provide safe operation across the full range of possible operating conditions, yet manual specification of safe operating regions is error-prone and incomplete. This work innovates by automating the discovery of safe initial conditions through formal analysis of system dynamics. The symbolic approach enables handling continuous state spaces and complex temporal properties infeasible with manual analysis.
This paper develops algorithms for synthesizing safe sets of operations for embedded systems by exploring the infinite state space of continuous dynamical systems to find initial states satisfying temporal properties. The work presents symbolic algorithms for computing forward and backward reachable sets of continuous systems and identifies initial conditions enabling systems to satisfy safety and liveness properties. The approach uses level set methods to represent continuous state spaces and symbolic computation for efficient exploration.
The algorithms successfully identify safe sets of initial conditions for continuous dynamical systems satisfying both safety and liveness properties. Results demonstrate effective computation of constrained reachable sets using level set methods and symbolic algorithms. The approach enables systematic identification of operating regions ensuring system safety.
@inproceedings{Dubey2009b,
author = {Dubey, Abhishek},
booktitle = {16th Annual {IEEE} International Conference and Workshop on the Engineering of Computer Based Systems, {ECBS} 2009, San Francisco, California, USA, 14-16 April 2009},
title = {Algorithms for Synthesizing Safe Sets of Operation for Embedded Systems},
year = {2009},
pages = {149--155},
abstract = {A large number of embedded computing systems are modeled as hybrid system with both discrete and continuous dynamics. In this paper, we present algorithms for analyzing nonlinear time-invariant continuous-time systems by employing reachability algorithms. We propose synthesis algorithms for finding sets of initial states for the continuous dynamical systems so that temporal properties, such as safety and liveness properties, are satisfied. The initial sets produced by the algorithms are related to some classical concepts for continuous dynamical systems, such as invariant sets and domains of attraction.},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/bib/conf/ecbs/Dubey09},
category = {conference},
contribution = {lead},
doi = {10.1109/ECBS.2009.43},
file = {:Dubey2009b-Algorithms_for_Synthesizing_Safe_Sets_of_Operation_for_Embedded_Systems.pdf:PDF},
keywords = {embedded systems, formal methods, reachable sets, safety, temporal properties, continuous dynamics},
project = {cps-reliability},
timestamp = {Wed, 16 Oct 2019 14:14:51 +0200},
url = {https://doi.org/10.1109/ECBS.2009.43}
}