|
 
|
[ABS08] Towards Maude-Tla based Foundation for Complex Concurrent Systems Specification and Certification
Conférence Internationale avec comité de lecture : ITNG'08, 5th International Conference on Information Technology: New Generations, Las Vegas, USA, January 2008, pp.1305-1307, Series IEEE,
motcle:
Résumé:
This paper contributes towards a multi-paradigm approach for the specification validation verification and refinement of concurrent agile systems. It brings together two complementary rigorous and largely accepted frameworks: MeseguerÂ’s true-concurrent Rewriting Logic (RL) with its Maude prototype and LamportÂ’s Temporal Logic of Actions (Tla) with its current prototype Tla+. At the specification / validation phase, we adopt a variant of Maude that we endow with strategy for controlling rules and state splitting / recombining for exhibiting full intra-concurrency. For the verification / refinement phase, we automatically derive TlaÂ’s formulas from validated Maude specification, on which crucial properties are checked using TlaÂ’s deductions and invariants. A production system is considered as proof-of-concept.
For further information, please visit this web site.
For further information, please visit this web site.
BibTeX
| @inproceedings { | |||
| ABS08, | |||
| title | = | "{Towards Maude-Tla based Foundation for Complex Concurrent Systems Specification and Certification}", | |
| author | = | " N. Aoumeur and K. Barkaoui and G. Saake ", | |
| booktitle | = | "{ITNG'08, 5th International Conference on Information Technology: New Generations, Las Vegas, USA}", | |
| year | = | 2008, | |
| month | = | "January", | |
| series | = | "IEEE", | |
| issue | = | 5, | |
| pages | = | "1305-1307", | |
| } | |||
