SynchAADL2Maude is an Eclipse plug-in that uses Real-Time Maude to simulate and model check Synchronous AADL models. Synchronous AADL is a variant of the industrial modeling standard AADL that supports the modeling of synchronous embedded systems. In particular, Synchronous AADL can be used to define in AADL the synchronous models in the PALS methodology, in which the very hard tasks of modeling and verifying an asynchronous distributed real-time system that should be virtually synchronous can be reduced to the much simpler tasks of modeling and verifying the underlying synchronous design.
Our tool requires the following tools and plug-ins:
The SynchAADL2Maude plugin also includes Real-Time Maude 2.3 tool. To install this plugin to OSATE, please copy every jar file in the archive into the plugins folder of Eclipse.
The usage of the SynchAADL2Maude tool can be found in the demo slides, in which we illustrate SynchAADL2Maude with the active standby example below.
The executable Real-Time Maude is provided here, where synch-aadl-interpreter.maude is the main semantics file. To execute the file, you must first start Maude and load Real-Time Maude as explained in Real-Time Maude web page.
Some Synchronous AADL examples are provided below, which can be imported into an OSATE workspace as AADL projects. Each archive file in the following contains AADL source code (in aadl folder) and the automatically generated Real-Time Maude specification (in verification folder), including property specification.
The following technical report gives more details about Synchronous AADL and its Real-Time Maude semantics, and the SyncAADL2Maude that integrate the whole Real-Time Maude verification process into OSATE modeling environent for AADL.