Details

Autor(en) / Beteiligte

• Aoumeur, N.
• Barkaoui, K.
• Saake, G.

Titel

Towards Maude-Tla based Foundation for Complex Concurrent Systems Specification and Certification

Ist Teil von

• Fifth International Conference on Information Technology: New Generations (itng 2008), 2008, p.1305-1307

Ort / Verlag

IEEE

Erscheinungsjahr

2008

Link zum Volltext

• IEEE_Xplore

Quelle

IEEE Explore

Beschreibungen/Notizen

• 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.