EmbLab/Tech: Difference between revisions
No edit summary |
No edit summary |
||
| (3 intermediate revisions by the same user not shown) | |||
| Line 5: | Line 5: | ||
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 | |||
The PCT patent regarding this method has been published [http://www.wipo.int/pctdb/en/wo.jsp?WO=2009095084&IA=EP2008051300&DISPLAY=STATUS here].<BR> | |||
A technical report that explains how it works is available [http://dii.ing.unimo.it/~emblab/CRIS-2008-02-01.pdf here]. | |||
Latest revision as of 07:30, 21 June 2010
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.
The PCT patent regarding this method has been published here.
A technical report that explains how it works is available here.