|
Published Articles >> Table of Contents >> Abstract
Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05)
pp. 250-260
From RT-LOTOS to Time Petri Nets New Foundations for a Verification Platform
T. Sadani, ENSICA, Cedex, France
P. De Saqui-Sannes, ENSICA, Cedex, France
J.-P. Courtiat, LAAS-CNRS, Cedex, France
Full Article Text:
 
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SEFM.2005.22
Send link to a friend
| Abstract |
|
The formal description technique RT-LOTOS has
been selected as intermediate language to add
formality to a real-time UML profile named TURTLE.
For this sake, an RT-LOTOS verification platform has
been developed for early detection of design errors in
real-time system models. The paper discusses an
extension of the platform by inclusion of verification
tools developed for Time Petri Nets. The starting point
is the definition of RT-LOTOS to TPN translation
patterns. In particular, we introduce the concept of
components embedding Time Petri Nets. The
translation patterns are implemented in a prototype
tool which takes as input an RT-LOTOS specification
and outputs a TPN in the format admitted by the TINA
tool. The efficiency of the proposed solution has been
demonstrated on various case studies.
|
 Additional Information
|
Citation:
T. Sadani, P. De Saqui-Sannes, J.-P. Courtiat,
"From RT-LOTOS to Time Petri Nets New Foundations for a Verification Platform,"
sefm,
pp. 250-260,
Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05),
2005
|
|
