Commit cb42814d authored by Jerome Hugues's avatar Jerome Hugues

Add various examples, basic blocks of a library and REAL theorems

parent 6c6e03b0
Jerome Hugues <hugues.jerome@gmail.com>
Quick installation instructions for AADLib
==========================================
Please refer to the AADLib user's guide for more detailed
installation instructions.
BUILD REQUIREMENTS:
===================
- Ocarina 2.0w
Optionnaly autoconf/automake if you rebuld from a fresh copy of the
repository.
BUILD AND INSTALLATION INSTRUCTIONS:
====================================
- Install Ocarina as specified by its documentation and make sure its
'bin' installation directories is located at the top of your PATH
environment variable.
- Issue
./configure
make && make install
- Type ./configure --help to get the list of possible options.
If you modify source files, build AADLib after a checkout or
make distclean, or the directory hierarchy of the source files, you
should re-generate autoconf and automake files (configure,
Makefile.in...); to do this, from the main directory, run:
./support/reconfig
For more details, please refer to AADLib's documentation.
AUTOMAKE_OPTIONS = no-dependencies
ACLOCAL_AMFLAGS = -I support
CLEANFILES = config-stamp
SUBDIRS = src examples
DIST_SUBDIRS = $(SUBDIRS)
clean-local:
-rm -f *~
EXTRA_DIST = $(srcdir)/README
This diff is collapsed.
* Add better documentation and comment in all models
* Enhance model reusability by rewriting models
* Add tests for aadlrev (AADL Inspector) and OSATE2
* Add Dining Philosophers example from Peter
* Complete Ardupilot
* Add models from SEI technical reports
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
AC_PREREQ(2.57)
AC_INIT(AADLib, 0.0.1, hugues.jerome@gmail.com)
AC_CONFIG_SRCDIR(src)
AC_CONFIG_AUX_DIR(support)
##########################################
# Initialization.
##########################################
AC_CANONICAL_SYSTEM
AM_INIT_AUTOMAKE([1.9 tar-pax] foreign)
##########################################
# Check fo various programs.
##########################################
AC_CHECK_PROG(MV, mv, mv)
AC_CHECK_PROG(RM, rm, rm)
AC_CHECK_PROG(CP, cp, cp)
##########################################
# Check for GNU Make
##########################################
AM_GNU_MAKE
##########################################
# Check for Ocarina
##########################################
AM_PATH_OCARINA(1.1, ,AC_MSG_ERROR([Ocarina 1.1 or later is not installed on your system]))
##########################################
# Windows requires specific targets
##########################################
case "$host_os" in
cygwin* | mingw*)
windows=true
;;
*)
windows=false
;;
esac
AM_CONDITIONAL(WINDOWS, test x$windows = xtrue)
############################################
# Set the value corresponding to cygpath -u
############################################
if test x"$CYGPATH_W" = x"echo"; then
CYGPATH_U="echo"
else
CYGPATH_U="cygpath -u"
fi
AC_SUBST(CYGPATH_U)
###############################################################
# Force the installation prefix to be equal to the Ocarina one
###############################################################
prefix='$(OCARINA_PREFIX)'
##########################################
# Output generated files
##########################################
dnl Important! One file per line, nothing before
dnl or after except whitespace! This section
dnl may, one day, be edited automatically to remove
dnl some entries.
AC_OUTPUT([
Makefile
examples/Makefile
examples/aocs/Makefile
examples/ardupilot/Makefile
examples/arinc653_annex/Makefile
examples/arinc653_annex/example_1/Makefile
examples/arinc653_annex/example_2/Makefile
examples/asl/Makefile
examples/behavior_annex/Makefile
examples/data_modeling_annex/Makefile
examples/fcs/Makefile
examples/flow_analysis/Makefile
examples/line_follower/Makefile
examples/mixin/Makefile
examples/memory/Makefile
examples/producer_consumer/Makefile
examples/radar/Makefile
examples/rap/Makefile
examples/ravenscar/Makefile
examples/rma/Makefile
examples/redundancy/Makefile
examples/round_robin/Makefile
examples/time_triggered/Makefile
examples/uxv/Makefile
examples/uxv/emaxxv2/Makefile
examples/uxv/minirocket/Makefile
examples/uxv/quadrirotorv0/Makefile
examples/uxv/quadrirotorv1/Makefile
examples/uxv/traxsterv3/Makefile
examples/voter/Makefile
src/Makefile
src/aadl/Makefile
src/property_set/Makefile
src/real/Makefile
])
AC_MSG_NOTICE(%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%)
AC_MSG_NOTICE(AADLib configuration is complete!)
AC_MSG_NOTICE(GNU make command name: "$GNU_MAKE")
AC_MSG_NOTICE(%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%)
SUBDIRS= \
aocs \
ardupilot \
arinc653_annex \
asl \
behavior_annex \
data_modeling_annex \
fcs \
flow_analysis \
line_follower \
mixin \
memory \
producer_consumer \
ravenscar \
radar \
rap \
redundancy \
rma \
round_robin \
time_triggered \
uxv \
voter
EXTRA_DIST=$(srcdir)/Makefile.common
SAMPLE_DIR = ${shell $(CYGPATH_U) '$(OCARINA_PREFIX)/examples/ocarina/aadlib'}
install-data-local:
$(INSTALL) -d $(DESTDIR)$(SAMPLE_DIR)
uninstall-local:
rm -rf $(DESTDIR)$(SAMPLE_DIR)
clean-local:
-rm -rf *~
OCARINA = ocarina
OCARINA_FLAGS = -aadlv2 -y -I$(top_srcdir)/src/property_set \
-I$(top_srcdir)/src/aadl -I$(srcdir) $(AADL_LIB)
check-local: $(AVAILABLE_TARGETS)
help:
@echo "Available targets: " $(AVAILABLE_TARGETS)
parse-aadl:
$(OCARINA) $(OCARINA_FLAGS) $(AADL_SOURCES)
instantiate-aadl:
$(OCARINA) $(OCARINA_FLAGS) -i -r $(AADL_ROOT) $(AADL_SOURCES)
c:
$(OCARINA) $(OCARINA_FLAGS) -g polyorb_hi_c -r $(AADL_ROOT) \
$(AADL_SOURCES)
build_c:
$(OCARINA) -b $(OCARINA_FLAGS) -g polyorb_hi_c -r $(AADL_ROOT) \
$(AADL_SOURCES)
ada:
$(OCARINA) $(OCARINA_FLAGS) -g polyorb_hi_ada -r $(AADL_ROOT) \
$(AADL_SOURCES)
build_ada:
$(OCARINA) -b $(OCARINA_FLAGS) -g polyorb_hi_ada -r $(AADL_ROOT) \
$(AADL_SOURCES)
arinc653_conf:
$(OCARINA) -b $(OCARINA_FLAGS) -g arinc653_conf -r $(AADL_ROOT) \
$(AADL_SOURCES)
cheddar:
$(OCARINA) $(OCARINA_FLAGS) -g cheddar -r $(AADL_ROOT) \
$(AADL_SOURCES)
cheddarlite -request all -file ./*_cheddar.xml
real:
$(OCARINA) $(OCARINA_FLAGS) -g real_theorem \
-real_lib $(top_srcdir)/src/real/aadl_theorems.real \
-real_lib $(top_srcdir)/src/real/arinc653_theorems.real \
-real_lib $(top_srcdir)/src/real/bare_board_theorems.real \
-real_lib $(top_srcdir)/src/real/data_model_theorems.real \
-real_lib $(top_srcdir)/src/real/flow_latency.real \
-real_lib $(top_srcdir)/src/real/memory_theorems.real \
-real_lib $(top_srcdir)/src/real/ravenscar_theorems.real \
-r $(AADL_ROOT) \
$(AADL_SOURCES)
clean-local:
-rm -rf *~ *_cheddar.xml
if test ! "$(CLEANDIRS)" = ""; then \
rm -rf $(CLEANDIRS); \
fi
EXTRA_DIST= $(AADL_SOURCES) $(OTHER_FILES)
This diff is collapsed.
README for AADLib examples
==========================
These examples illustrate some use of the AADLib AADL component
libraries, adapted from exising AADL models (either v1 or v2) to
AADLv2, and the AADLib AADL components library.
For each example:
- "make help" return the list of available targets for this example,
from the following list:
- "make parse-aadl" : compile the example using Ocarina
- "make c" : generate architecture C code derived from the AADL
model, using the Ocarina/C code generator
- "make build_c" : generate and compile C code
- "make ada" : generate architecture Ada code
- "make build_ada" : generate and compile C code
- "make real" : check REAL theorems applicable to this model
- "make cheddar" : check scheduling of the corresponding model
- "arinc653_conf" : generate ARINC653 XML descriptor from AADLv2 model
- "make clean" : remove generated files
In addition, the following target is always available:
- "make check" : run all available targets, for regression testing
Here is a short description of each example
* aocs: model of an Attitude Orbital Constrol System, derived from
design document from
http://control.ee.ethz.ch/~ceg/AocsFramework/index.html
(XXX)
* ardupilot: models the ardupilot UAV platform, adapted from the POK
project (see http://pok.safety-critical.eu)
* arinc653_annex: models from the ARINC653 annex document for AADLv2
* asl: work in progress REAL theorems in preparaton for the ASL annex
as part of SAE AS2/C committee work
* avionices_nasa:
* behavior_annex: models from the Behavior annex language for AADLv2
* data_modeling_annex: models from the Data Modeling annex document
for AADLv2
* fcs: models a naive Flight Control Systems, adapted from a lab on
scheduling analysis tools developped by C. Pagetti from ONERA; and
adapted for AADL teaching classes by J. Hugues at ISAE. Only the
architecture is developped, to be analyzed with Cheddar.
* line_follower: a line follower robot for the Arduino platform, using
some parts available from SparkFun Electronics.
* mixin: this example demonstrates how to support multiple inheritace
in AADLv2, using the mixin pattern defined in many object-oriented
languages like Ada.
* memory: this examples demonstrates how to define logical and
hardware memory layout, and how to ensure they match. This example
was build in collaboration between F. Singhoff and S. Rubini (UBO)
and J. Hugues (ISAE)
* radar: a naive model of a radar system, made in collaboration with
F. Singhoff from UBO, P. Disseaux from Ellidiss and Nader KHAMMASSI
from Virtualys and J. Hugues (ISAE). Adapted to AADLv2
* rap: Ravenscar Avionics Platform, written by Olivier Gilles during
his PhD. This models builds upon the Generic Avionics Platform.
(XXX)
* ravenscar: case study issued from the ``Guide for the use of the Ada
Ravenscar Profile in high integrity systems'' written by Alan Burns,
Brian Dobbing and Tullio Vardanega; adapted to AADLv1 by Bechir
Zalila duing his PhD. This models has been translated to AADLv2, and
extended to include REAL theorems to check Ravenscar patterns.
* rma: two tasks with different period on the same node, can be
checked by Cheddar, or can generate code for either PolyORB-HI/C or
Ada.
* time_triggered: shows how to implement a time-triggered architecture
using delayed connections.
* uxv: models a series of UAV and UGV from ISAE DMIA lab. Initial
models were build by Cedric Chedaleux, Fabrice Cotdeloup and Sladana
Yousri-Stojkovic while students at ISAE.
AADL_SOURCES = $(srcdir)/aocs.aadl
AADL_ROOT = aocs_subsystem.impl
OTHER_FILES = \
$(srcdir)/dataaocs.aadl \
$(srcdir)/hardware.aadl \
$(srcdir)/software.aadl
include $(srcdir)/../Makefile.common
AVAILABLE_TARGETS= parse-aadl
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
AADL_SOURCES = $(srcdir)/main.aadl
AADL_ROOT = ardupilot.i
OTHER_FILES = \
$(srcdir)/ardupilot_platform.aadl \
$(srcdir)/ardupilot_software.aadl \
$(srcdir)/flt-mgmt.c \
$(srcdir)/gps.c \
$(srcdir)/throttle.c \
$(srcdir)/userdefined.mk \
$(srcdir)/yaw.c
include $(srcdir)/../Makefile.common
AVAILABLE_TARGETS= parse-aadl real
# build_c: probleme pour prendre en compte userdefined.mk lors d'un distcheck
distclean-local:
-rm -rf ardupilot_i
This diff is collapsed.
package ardupilot_platform
public
processor cpu end cpu;
memory mem end mem;
memory implementation mem.i
end mem.i;
end ardupilot_platform;
This diff is collapsed.
This diff is collapsed.
#include <stdio.h>
#include <math.h>
#include "types.h"
float glob_longitude = 1.4;
float glob_latitude = 2.5;
int glob_altitude = 3;
void gps_simulation (ardupilot_software__gps_position_i* pos)
{
pos->altitude = glob_altitude;
pos->latitude = glob_latitude;
pos->longitude = glob_longitude;
printf ("[GPS] Simulate latitude %f, longitude %f\n",
pos->latitude, pos->longitude);
}
void gps_backdoor (float yaw)
{
glob_longitude += sin(yaw)/20.0;
glob_latitude += cos(yaw)/20.0;
}
package Main
public
with Processors::Atmega;
with Ardupilot_Software;
with Deployment;
---------------
-- Ardupilot --
---------------
system Ardupilot
end Ardupilot;
system implementation Ardupilot.i
subcomponents
CPU : processor Processors::Atmega::ATMEGA328p.impl
{Deployment::Execution_Platform => Native;
Scheduling_Protocol => (POSIX_1003_HIGHEST_PRIORITY_FIRST_PROTOCOL);
-- Thread_Limit => 42;
Thread_Limit => 4;
};
process_Ardupilot : process Ardupilot_software::Ardupilot_code.impl;
properties
Actual_Processor_Binding => (reference (CPU)) applies to process_Ardupilot;
end Ardupilot.i;
end Main;
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.