Where academic tradition
meets the exciting future

Designing Controllers for Reachability

Cristina Cerschi Seceleanu, Designing Controllers for Reachability. In: Proceedings of the 29th Annual International Computer Software and Applications Conference (COMPSAC 2005), IEEE Computer Society, 2005.

Abstract:

We propose a deductive method for constructing reliable reachability controllers, with application to fault-tolerant discrete systems. Designing the controller reduces to finding a strategy to win specific games defined by sequential dually nondeterministic statements. During the game, the controller tries to achieve its goal, in spite of the adversarial behavior of the environment. Being a reachability game, the goal of the controller is modeled by a special kind of liveness property. We show that the controller has a way to enforce the required property, provided that adequate invariance and termination properties hold. The winning strategy is obtained by propagating certain assertions into the statement that models the controller's behavior. We illustrate our method on a data-processing application.

BibTeX entry:

@INPROCEEDINGS{inpCerschiSeceleanu05b,
  title = {Designing Controllers for Reachability},
  booktitle = {Proceedings of the 29th Annual International Computer Software and Applications Conference (COMPSAC 2005)},
  author = {Cerschi Seceleanu, Cristina},
  publisher = {IEEE Computer Society},
  year = {2005},
}

Belongs to TUCS Research Unit(s): Software Construction Laboratorium

Edit publication