Automating Verification of Cooperation, Control, and Design in Traffic Applications - Formal Methods and Hybrid Real-Time Systems - page 161

in [37,38]. Frehse [19] provides an assume-guarantee based approach for hybrid
systems which do not share variables. The restriction to event-based communi-
cation is reasonable for controller models; however, as soon as closed loop models
are considered, plant models will typically share system states; in particular, for
collision avoidance protocols, it is exactly the shared physical state space which
is subject to the analysis. The extension to shared variables provided in [20]
requires unique statically assigned owners of shared variables - only owners are
allowed to write on shared variables.
Frehse's approach only addresses refinement of specifications. For hybrid sys-
tems with shared variables, the notions of refinements presented do not track
continuous evolutions, but only require matching continuous states at end-points
of continuous evolutions. Stauner [51,52] studies more general notions of refine-
ment, which in particular aim at bridging the gap between local control and
design models. The key concepts of using bounded perturbations to provide
room for discretization and inter-sampling errors in the transition to design mod-
els are promising. Systematic methods are proposed for constructing a discrete
time model refining the relaxed local control model under certain conditions are
provided. However, a general notion of refinement, applicable to design mod-
els not constructed using Stauner's approach, is not given. Since design models
also must cater for additional aspects such as fault-tolerance and diagnosis, a
general theory for refinement between design models and local control models is
desirable. Additionally, a compositional extension of this framework is needed.
We plan to elaborate our research along multiple dimensions. First, we will
extend the model at the cooperation layer emphasizing the dynamic aspect of
trac applications, in which trac agents enter and leave “interaction areas”,
and lift the technique of reducing collision freedom to arguments on criticality
functions and local control properties to this richer semantic setting. Secondly,
while we demonstrated the scalability of our AIG based verification methods
to linear hybrid automata with large discrete state spaces (e.g., to a flap con-
troller with 2 20 discrete states [11]), future work will address support for plant
dynamics governed by linear differential equations. Thirdly, we plan to research
into robust refinement relations and non-standard semantics of hybrid automata
to extend compositional refinement techniques to a theory providing semantic
bridges across the layered design space of cooperating trac agents.
References
1. Alur, R., Grosu, R., Hur, Y., Kumar, V., Lee, I.: Modular specification of hybrid
systems in CHARON. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS,
vol. 1790, pp. 6-19. Springer, Heidelberg (2000)
2. Alur, R., Grosu, R., Lee, I., Sokolsky, O.: Compositional modeling and refinement
for hierarchical hybrid systems. Journal of Logic and Algebraic Programming 68(1-
2), 105-128 (2006)
3. Balluchi, A., Benvenuti, L., Engell, S., Geyer, T., Johansson, K., Lamnabhi-
Lagarrigue, F., Lygeros, J., Morari, M., Papafotiou, G., Sangiovanni-Vincentelli,
A., Santucci, F., Stursberg, O.: Hybrid control of networked embedded systems.
European Journal on Control, Fundam. Issues in Control 11(4-5), 478-508 (2006)