Loading...
Please wait, while we are loading the content...
Similar Documents
The uml profile for modeling and analysis of real-time.
| Content Provider | CiteSeerX |
|---|---|
| Author | Yu, Huafeng Talpin, Jean-Pierre Besnard, Loïc Gautier, Thierry Marchand, Hervé Guernic, Paul Le |
| Abstract | and Embedded systems (MARTE) defines a mathematically expressive model of time, the Clock Constraint Specification Language (CCSL), to specify timed annotations on UML diagrams and thus provides them with formally defined timed interpretations. Thanks to its expressive capability, the CCSL allows for the specification of static and dynamic properties, of deterministic and non-deterministic behaviors, or of systems with multiple clock domains. Code generation from such multiclocked specifications (for the purpose of synthesizing a simulator, for instance) is known to be a difficult issue. We address it by using the approach of controller synthesis. In our framework, a timed CCSL specification is regarded as a property whose satisfaction should be enforced for any UML diagram carrying it as annotation. To do so, CCSL statements are first translated into dynamical polynomial systems. Such systems can be manipulated using the model-checker Sigali to synthesize an executable property (a controller) which enforces the satisfaction of the specified timing constraints on the UML diagram with which it is executed. Index Terms—MARTE; Polychrony; CCSL; GALS; controller synthesis; I. |
| File Format | |
| Access Restriction | Open |
| Subject Keyword | Uml Diagram Uml Profile Controller Synthesis Difficult Issue Expressive Capability Non-deterministic Behavior Ccsl Statement Dynamical Polynomial System Timed Annotation Model-checker Sigali Timed Interpretation Dynamic Property Clock Constraint Specification Language Expressive Model Timed Ccsl Specification Multiple Clock Domain Specified Timing Constraint Code Generation Executable Property Embedded System Index Term Marte |
| Content Type | Text |