SLA++P is a workshop dedicated to synchronous languages and
the model-driven high-level programming of reactive and embedded systems.
Firmly grounded in clean mathematical semantics, synchronous languages are
receiving increasing attention in industry ever since they emerged in the
80s. Lustre, Esterel, Signal are now widely and successfully used to program
real-time and safety critical applications of commercial scale, from nuclear
power plant management layer to Airbus air flight control systems. At the
same time, model-based programming is making its way in other fields of software
engineering, too, often involving cycle-based synchronous paradigms.
SLA++P extends the former SLAP workshop series on Synchronous
Languages, Applications, and Programming but is not limited to synchronous
approaches. It is open to other engineering design techniques with strong
semantical foundations providing a way to go from high-level description to
provable executable code.
Synchronous languages have been introduced
in the 80s to program embedded systems. Such systems are characterized by
their continuous reaction to their environment, at a speed determined by the
latter. Synchronous languages have recently seen a tremendous interest from
leading companies developing automatic control software for critical applications.
For instance, Schneider Electric uses a Lustre-based tool, named Scade, to
develop the control software for nuclear plants. Aerospatiale also uses this
tool to develop the flight control of the new Airbus planes. Dassault Aviation
uses Esterel Studio to program the flight control software of the Rafale fighter.
Snecma uses Sildex, a Signal-based tool to develop airplane engines. ST Microelectronics,
Texas Instrument, Motorola, Intel, are also interested in the Esterel technology
for chip design. The key advantage pointed by these companies is that the
synchronous approach has a rigorous mathematical semantics which allows the
programmers to develop critical software faster and better.
Indeed, the semantics of the languages is used as a formal model upon which
all the programming environments are defined. The compilation involves the
construction of these formal models, and their analysis for static properties,
their optimization, the synthesis of executable sequential implementations,
the automated distribution of programs. It can also build a model of the dynamical
behaviors, in the form of a transition system, upon which are based the analysis
of dynamical properties, e.g., through model-checking based verification,
or discrete controller synthesis. Hence, synchronous programming is at the
cross-roads of many approaches in compilation, formal analysis and verification
techniques, and software or hardware implementations generation. The approach
is related to formal methods for reactive systems like Statecharts, StateFlow,
UML StateCharts.
Topics of Interest
After SLAP’2002
in Grenoble, SLAP’2003
in Porto, SLAP’2004
in Barcelona,SLAP’2005 in Edinburgh, SLAP'2006
in Vienna, this revised SLA++P'2007 edition of the workshop series intends
to cover a wider range of programming models than previously done. This corresponds
to the current interest in component programming for large scale embedded
systems, the link between simulation tools (a la Simulink/StateFlow) and compiler
tools (a la Scade), languages for describing the system and its environment,
integrated tools for both compilation and simulation, etc. To summarise, SLA++P
2007 is open to all approaches based strongly on semantics and providing a
way to go from a high-level description of the system to provable executable
code.
The
workshop topics cover, among others, the following issues:
synchronous and asynchronous models for time and concurrency
novel language paradigms blending synchrony with asynchrony and non-determinism,
semantic abstraction and refinement,
synchronous languages and programming formalisms,
compilation techniques,
formal specification and verification,
test and validation of programs,
case-studies, industrial and teaching experience
design methodologies, visualisation of complex reactive systems
component-based development of embedded systems
Format of the
Workshop
This one-day workshop will feature a keynote address from an invited speaker,
technical presentations, and a panel discussion.
Schedule
Paper submission:December 11,
2006.
Notification of acceptance:February
5, 2007
Final paper due: February 26, 2007
Workshop: March 31, 2007
Submission
Contributions
are sought in the form of regular paper submissions which may be extended abstracts
or full papers describing original research results or work in progress, and
should be no longer than 15~pages. Selected papers from SLA++P'2007 will be
invited for submission to a special issue of the EURASIP
Journal on Embedded Systems which will be published on the topic of this
workshop.
Programme
The programme committee has accepted 9 papers out of 16 submissions. Here
is the programme that will take place on Saturday March 31, 2007.
09:00 - 09:05
Welcome and Opening
M.Mendler
09:05 - 09:50
Invited Talk:
Formal Verification of Synchronous Models: An
Industrial Application of Formal Methods
Worst Case Reaction Time Analysis of Concurrent Reactive Programs
M.Boldt, C.Traulsen, R.von Hanxleden
11:40 - 12:20
Executable Specifications for Real-Time Distributed Systems
A.Ray, R.Cleaveland
12:20 - 12:30
Presentation: SYNCHRON'07
and SLAP'08
M.Mendler
12:30 - 14:00
Lunch
14:00 - 14:40
Instantaneous Transitions in Esterel
O.Tardieu, S.A.Edwards
14:40 - 15:20
Specifying and executing reactive scenarios with Lutin
P.Raymond, Y.Roux, E.Jahier
15:20 - 16:00
Modifying Contracts with Larissa Aspects
D.Stauch
16:00 - 16:30
Afternoon Coffee Break
16:30 - 17:10
Lustre as a System Modeling Language: Lussensor, a Case-Study with
Sensor Networks
F.Maraninchi, L.Samper, K.Baradon, A.Vasseur
17:10 - 17:50
Towards mutation analysis for LUSTRE programs
L.du Bousquet, M.Delaunay
17:50 - 18:30
Extending Lustre with Timeout Automata
J.Gao, M.Whalen, E.Van Wyk
Invited Speaker (Biography)
Dr. Steven Miller is a Senior Principal Software Engineer in the Advanced
Technology Center of Rockwell Collins and has almost 30 years of experience
in software development. He received his Ph.D. in computer science from the
University of Iowa in 1991, as well as a B.A. in physics and mathematics in
1974.
His current research interests include model-based development, formal methods,
and software testing. He was principle investigator on a 5-year project sponsored
by NASA Langley’s Aviation Safety Program and Rockwell Collins to investigate
advanced methods and tools for the development flight critical systems. Prior
to that he lead several research efforts at Rockwell Collins, including a
collaborative effort with SRI International and NASA to formally verify the
microcode in the AAMP5 and AAMP-FV microprocessors using the PVS verification
system.
Formal Verification of Synchronous
Models: An Industrial Application of Formal Methods (Abstract)
Model-based development, in which models of system behavior are created early
in the development process, simulated, then used to automatically generate
code and test cases, is becoming increasingly common in the industrial development
of embedded software. At the same time, formal verification tools such as
model-checkers are rapidly growing more powerful. The convergence of these
two trends opens the door for the practical application of formal verification
techniques early in the life-cycle for important classes of systems. In particular,
synchronous modeling languages seem to be especially well suited to both industrial
use and formal verification. This talk will describe how Rockwell Collins
has applied formal verification tools developed under NASA’s Aviation Safety
Program to commercial avionics systems in order to reduce costs and improve
quality by detecting requirements and design errors early in the lifecycle.
The organising committee invites up to 5 European graduate students (or students
from an institution affiliated to Artist)
to participate in the workshop. The grants provided by Artist
consist of 600 euros each, which are going to be paid in British Pounds by
way of expense claims after the workshop has taken place. In order to get
one of these grants, you must submit (by e-mail to joaquin.aguado@wiai.uni-bamberg.de)
the following:
Generals: Name, nationality, affiliation, e-mail and research-status
(e.g. PhD student).
A short description of your work explaining your motivation for participating
in this workshop.
If applicable a list of previous publications.
A CV.
Please send all the above in one e-mail no later than February
20th. You will get an answer before the ETAPS registration deadline
(February 26th).
Last modification: 5 April 2007. Information
maintained by Joaquin
Aguado
