EmbLab/Tech: Difference between revisions
(New page: {{EmbLab}} ==Method for ensuring safety and liveness rules in a state based design == Aim of this document is to describe a method which works upon an abstract operational and structural...) |
No edit summary |
||
| Line 4: | Line 4: | ||
Aim of this document is to describe a method which works upon an abstract operational and structural model of the control of one or more sets of state machines, named assemblages, by means of other state machines, named controllers. According to the model, such controllers may be further grouped into assemblages themselves and be controlled, on their turn, by other controllers, and so on. The method is based on state constraints, which are propositions about the global state of an assemblage and enforces safety in a state based design, that is it checks that such constraints are always verified, that is when the controller is in a given state the controlled machines in the assemblage do not violate the constraint of such state. It moreover shows how to ensure that a reactive behavior is correctly implemented, that is when the assemblage moves, in an uncontrollable way, to a global state which violates the constraint of the current state of the controller, then there is a transition in the controller that is triggered and move the control out of the violated state. The method enforces also liveness in a state based design, by checking that any part of the constraint of a given state may be reached by the global state of the assemblage. | Aim of this document is to describe a method which works upon an abstract operational and structural model of the control of one or more sets of state machines, named assemblages, by means of other state machines, named controllers. According to the model, such controllers may be further grouped into assemblages themselves and be controlled, on their turn, by other controllers, and so on. The method is based on state constraints, which are propositions about the global state of an assemblage and enforces safety in a state based design, that is it checks that such constraints are always verified, that is when the controller is in a given state the controlled machines in the assemblage do not violate the constraint of such state. It moreover shows how to ensure that a reactive behavior is correctly implemented, that is when the assemblage moves, in an uncontrollable way, to a global state which violates the constraint of the current state of the controller, then there is a transition in the controller that is triggered and move the control out of the violated state. The method enforces also liveness in a state based design, by checking that any part of the constraint of a given state may be reached by the global state of the assemblage. | ||
[[http://dii.ing.unimo.it/~emblab/CRIS-2008-02-01.pdf CRIS-2008-02-01]] | |||
Revision as of 09:30, 30 June 2009
Home Staff Publications Technical reports Thesis
Method for ensuring safety and liveness rules in a state based design
Aim of this document is to describe a method which works upon an abstract operational and structural model of the control of one or more sets of state machines, named assemblages, by means of other state machines, named controllers. According to the model, such controllers may be further grouped into assemblages themselves and be controlled, on their turn, by other controllers, and so on. The method is based on state constraints, which are propositions about the global state of an assemblage and enforces safety in a state based design, that is it checks that such constraints are always verified, that is when the controller is in a given state the controlled machines in the assemblage do not violate the constraint of such state. It moreover shows how to ensure that a reactive behavior is correctly implemented, that is when the assemblage moves, in an uncontrollable way, to a global state which violates the constraint of the current state of the controller, then there is a transition in the controller that is triggered and move the control out of the violated state. The method enforces also liveness in a state based design, by checking that any part of the constraint of a given state may be reached by the global state of the assemblage.