Jump to : Download | Abstract | Contact | BibTex reference | EndNote reference |

YU:2011:INRIA-00594942:1

H. Yu, J-P. Talpin, L. Besnard, T. Gautier, H. Marchand, P. Le Guernic. Polychronous Controller Synthesis from MARTE CCSL Timing Specifications. In ACM/IEEE Ninth International Conference on Formal Methods and Models for Codesign (MEMOCODE), Pages 21-30, Cambridge, United Kingdom, July 2011.

Download [help]

Download paper: Doi page

Download paper: Adobe portable document (pdf) pdf

Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
This page is automatically generated by bib2html v216, © INRIA 2002-2007, Projet Lagadic

Abstract

The UML Profile for Modeling and Analysis of Real-Time 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

Contact

Hervé Marchand http://people.rennes.inria.fr/Herve.Marchand/

BibTex Reference

@InProceedings{YU:2011:INRIA-00594942:1,
   Author = {Yu, H. and Talpin, J-P. and Besnard, L. and Gautier, T. and Marchand, H. and Le Guernic, P.},
   Title = {Polychronous Controller Synthesis from MARTE CCSL Timing Specifications},
   BookTitle = {{ACM/IEEE Ninth International Conference on Formal Methods and Models for Codesign (MEMOCODE)}},
   Pages = {21--30},
   Address = {Cambridge, United Kingdom},
   Month = {July},
   Year = {2011}
}

EndNote Reference [help]

Get EndNote Reference (.ref)