Distributed Real-Time and Embedded (DRE) systems must enforce
constraints of both real-time and embedded paradigms.
They need to comply to specific requirements : strict
determinism, low resource consumption and full reliability.
Hence, non-functional requirements are necessary for DRE
systems, and the more constrained they are, the more
complex those requirements are.
Design a complete embedded real-time system is a complex
process, which involve modeling, verification, validation,
code generation and legacy code integration. Having only
one modeling framework ease integration and lower the
risks of model inconsistancies.
Yet it requires to define a constrained model so that
non-functional requirements could be enforced. The
AADL allows for the
description of complete systems from which executable
can be deduced.
Our work consist in designing a Domain-Specific Language (DSL) of AADL in order to define and automatically check these non-functional requirements.
REAL aims to check adequacy between different parts of architectural descriptions, with emphasis to conciseness and simplicity.
It is a language based on set manipulation. It allows to build sets whose elements are AADL instances (either connections, components or subprogram calls) by providing their first-order logic definition. Verifications can then be performed on either a set or all its elements by stating boolean expressions on them.
The basic unit of REAL is a theorem. A theorem is made of 3 parts :
Ocarina is a tool suite built in order to manipulate AADL models. Ocarina proposes AADL model manipulation, generation of formal models, performs scheduling analysis and generates distributed hi-integrity applications in Ada language. In our work, we focus on Ocarina as code generator for AADL and AADLv2 models.
Non-functional requirements are a critical part of any DRE systems. REAL allows to specify and test these requirement in the AADL model, and then the Ocarina construction insure that the generated code will follow the requirements. Since REAL performs verification directly on Ocarina tree, no bias can appear between the models used for verification and generation. We have developed REC (Requirement Enforcement Checker), an interpreter for REAL, and it is available in the download section.
REAL has been developed with Ocarina and GNAT (distributed by AdaCore). It has been tested under Linux.
The REAL interpreter is released under the GNAT Modified GPL. Here is an excerpt from the Licence.
Ocarina is a free software;you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version.
This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.
You should have received a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110, USA.
As a special exception, if other files instantiate generics from this unit, or you link this unit with other files to produce an executable, this unit does not by itself cause the resulting executable to be covered by the GNU General Public License. This exception does not however invalidate any other reasons why the executable file might be covered by the GNU Public License.
REAL has been developped by Olivier GILLES.
[GH08a] O. Gilles and J. Hugues. Validating requirements at model-level. Proceedings of the 4th workshop on Model-Oriented Engineering (IDM'08), june 2008.
[GH08b] O. Gilles and J. Hugues. Applying WCET analysis at architectural level. Proceedings of the 8th International Workshop on Worst-Case Execution Time Analysis (WCET'08), july 2008.