Conference Image Banner
12th International Conference
on Reliable Software Technologies
Geneva, 25-29 June 2007
ACM SIGAda 2007
Annual International Conference on
Software Development for Safety, Security,
and High Reliability Systems
4 - 8 November 2007
at Washington DC, USA
official website
 

Schedule

Monday
June 25th

T1

Morning

William Bail
An Overview of Model Driven Engineering

Room A101

T2

Morning

Tullio Vardanega
CbyC: A UML2 profile enforcing the Ravsenscar Computational Model

"Conference" Room

T3

Afternoon

William Bail
Verification and Validation for Reliable Software Systems

Room A101

T4

Afternoon

Matthew Heaney
Object Oriented Programming in Ada 2005

"Conference" Room

T5

Full day

Rod Chapman
Security by Construction

Room A102

Friday
June 29th

T6

Morning

Gerard Berry
Synchronous Design of Embeeded Systems: the Esterel/Scade Approach

Room A102

T7

Afternoon

Thomas Quinot and Jérôme Hugues
Building interoperable applications with PolyORB

Room A102

T8

Full day

Jolita Ralyté
Situational Method Engineering: Towards a Specific Method for Each System Development Project

Room A101

Morning tutorial sessions will start at 9:30 and end at 13:00. Afternoon sessions will start at 14:30 and end at 18:00.
There will be coffee breaks at 11:00 - 11:30 and at 16:00 - 16:30.


An Overview of Model Driven Engineering

William Bail,

The MITRE Corporation

(Monday June 25th, morning)

Abstract
Model Driven Engineering (MDE) in its various names, such as Model Driven Architecture®, has matured significantly over the past few years, and as a consequence has become much more widely used throughout industry. Some practitioners are claiming significant gains in productivity and product quality, while others cite more modest benefits. This tutorial examines MDE, looking at the mechanics of its process, revealing its constituent elements, and describing how it automates portions of the development process. It analyzes the parts of the process where the productivity and quality gains are realized, and also takes a critical look at the various claims that are being made about its benefits. The tutorial provides an objective assessment of the maturity of MDE, and objectively assesses the potential benefits of using this technology. The tutorial does describe any specific tool but rather describes the underlying technical basis.

Outline

  • Overview of software development
  • To provide a context for the rest of the briefing
  • To show where modeling techniques can provide benefits
  • Models and software engineering
  • Model Driven Engineering
  • Model Driven Architecture®

Why you should participate in this tutorial?
This tutorial will provide the attendee with the basic understanding of the technical underpinnings of Model Driven Engineering, and thereby provide a basis for selection of this technique for candidate software development projects. The tutorial will also provide an assessment of the level of maturity of the technology, and provide a perspective regarding where additional research is needed. Understanding the underlying principles, and the relative strengths and weaknesses of MDE, is essential to making informed decisions and selecting (or not selecting) MDE as a development strategy.

Presenter
Dr. Bail received a BS in Mathematics from Carnegie Institute of Technology, and an MS and Ph.D. in Computer Science from the University of Maryland. Since 1990, Dr. Bail has worked for The MITRE Corporation in McLean VA as a Computer Scientist in the Software Engineering Center (SWEC). MITRE is a not-for profit corporation chartered to provide systems engineering services to the U.S. Government agencies, primarily the DoD, the FAA, and the IRS. Within MITRE, the SWEC focuses on supporting various programs with consultation, particularly transitioning emerging technologies into practice. Dr. Bail’s technical areas of focus include dependable software design and assessment, error handling policies, techniques for software specification development, design methodologies, metric definition and application, and verification and validation. At MITRE, Dr. Bail is currently supporting the U.S. Navy, focusing on the practice of software engineering as applied to large real-time systems. Prior to 1990, Dr. Bail worked at Intermetrics Inc. in Bethesda MD.
Since 1989 he has served as an Adjunct Professor at the University of Maryland University College where he develops instructional materials and teaches courses in software engineering, in topics such as Software Requirements, Verification and Validation, Software Design, Software Engineering, Fault Tolerant Software, and others. Previously, Dr. Bail taught part-time at The University of Maryland from 1983-1986 in the Computer Science Department for undergraduate courses in discrete mathematics, computer architecture, and programming language theory.
Dr. Bail has presented tutorials on Cleanroom Software Engineering, Semi-Formal Development Techniques, Statistical Testing, and Requirements Engineering for Dependable Systems at SIGAda, Ada-Europe, and other conferences.


Correctness by construction: A UML2 profile enforcing the Ravenscar Computational Model

Tullio Vardanega,

University of Padua, Italy

(Monday June 25th, morning)

Abstract
This tutorial illustrates some  results from a core track of the EC FP6 ASSERT project, which aims to unite three distinct wavefronts in the engineering of high-integrity software systems:

  • the pursuit of a “correctness by construction” development paradigm;
  • the reliance on the UML2 notions of profile supported by meta-model ontologies;
  • the adoption of an educated approach to the use of concurrency centred around guaranteed compliance with the computational model defined the Ravenscar Profile.

The tutorial proceeds in three successive steps:

    • first we discuss how a UML2 profile can be constructed by mapping the basic ontologies of HRT-HOOD onto the UML2 metamodel;
    • subsequently we address and overcome some frustrating limitations inflicted by the HOOD heritage on the expressive power at model level and make an important step toward better integration of the HRT and OO dimensions of modern systems;
    • finally we show how Ada 2005 permits to amplify the benefits of correct-by-construction model-based code generation via factorization and instantiation.

Level
The tutorial is intended for an audience with some prior experience with the development of high-integrity real-time systems. It is possible that the tutorial will include the practical demonstration of some utilities in support of the subject development method.

Why you should participate in this tutorial?
There is growing awareness that the development of high-integrity real-time systems demands better methods that unite solid theoretical foundations with sufficient flexibility to leverage on some controlled form of Model-Driven Engineering. The tutorial illustrates the principles that inspire a novel development method as it stems from the ASSERT project partially funded by the European Commission as part of the IST objective of VI Framework Programme (FP6-IST-004033).

Presenter
Tullio Vardanega, from the Department of Pure and Applied Mathematics of the University of Padua, is an expert in the development of real-time embedded systems, and processes and methodologies for the engineering of software-intensive high-integrity systems. Before joining the University of Padua, he worked for a long time at ESA, the European Space Agency. He is Ada-Europe Board member and Editor of the Ada User Journal. He is active in ISO's Ada standardization working group (WG9), more specifically in the Ada Rapporteur Group (ARG, language maintenance) and the Annex H Rapporteur Group (HRG, guidance for high integrity applications in Ada).


Object-Oriented Programming in Ada 2005

Matthew Heaney,

On2 Technologies, USA

(Monday June 25th, afternoon)

Abstract
This tutorial discusses object­oriented programming in Ada05.  In addition to discussing classic features such as tagged types, class-wide programming, and access discriminants, the tutorial will include information about new procedure-call syntax, interface types, anonymous access types and anonymous subprogram parameters, extended return statements, limited-with and private-with package dependencies, and limited aggregates and box defaults.  The tutorial will also present idioms for implementing a type, constructing and destroying instances, designing subsystems, and for storage management and concurrency.

Why you should participate in this tutorial?
Attendees will gain a thorough understanding of how to use the myriad language features available for crafting abstractions in Ada, learning useful rules-of-thumb for their proper use.

Presenter
Matthew Heaney is the author of Charles, a container library for Ada which was the basis of the proposal selected by the ARG for the Ada 2005 standard container library. He has given many Ada tutorials on topics that include object-oriented programming, design patterns, and software systems and library design. Matt was recently awarded an Outstanding Ada Community Contribution Award by SIGAda, for his work in the development of container libraries for Ada.


Verification and Validation for Reliable Software Systems

William Bail,

The MITRE Corporation, USA

(Monday June 25th, afternoon)

Abstract
The practice of verification and validation (V&V) is a key aspect of any software development effort, and is tightly intertwined with the construction of the software. In this tutorial we examine the nature of V&V as applied to software systems with high expectations of dependability, and present techniques that have been shown to increase quality and dependability. We emphasize that V&V is more than just a “testing” activity, and includes practices that include testing as well as other valuable techniques, such as reviews, inspections and audits. We describe these practices, point out their individual strengths and weaknesses, and provide advice on how to select the appropriate practices based on the nature of the system under development. A key aspect of this selection process is correlating the techniques to the different types of requirements, recognizing that the requirements define the desired attributes of the system. We describe some challenges in applying V&V, and describe how to approach these challenges to improve the results. We also contrast “normal” V&V with “Independent V&V” (IV&V), an approach often used for large software development efforts.

Outline

  • Introduction to tutorial content
  • Overview of verification and validation
  • Practices: reviews, audits, and inspections
  • Practices: test
  • Special challenges
  • Planning for V&V

Why you should participate in this tutorial?
This tutorial will provide the attendee with the basic understanding of different verification and validation techniques, and advice on how to select and apply them based on the system to be developed. This information will assist in planning for complex systems development by providing a framework of verification steps that will balance cost efficiency with the need to demonstrate that systems are able to deliver their required high levels of dependability.

Presenter
See first Tutorial


Security by Construction

Rod Chapman,

Praxis HIS, UK

(Monday June 25th, full day)

Abstract
This tutorial will cover the use of "Correctness by Construction" (CbyC) techniques in the development of highly secure software systems. While the use of CbyC is well-known in the development of safety-related systems, it has also been deployed in the domain of highly secure systems.  The software world seems plagued by security problems caused by basic mistakes in software design and construction, but this tutorial will show how practices from the safety-critical domain can be used to tackle these problems.  In particular, the role of formal methods, programming language design, and strong static verification will be covered.  The tutorial will be illustrated with reference to CbyC security projects such as the MULTOS CA and the NSA Tokeneer system.
Description of Topic: Software security is one of the highest-profile and most important topics facing researchers today. The plague of "buffer overflow" and similar attacks that we read about every day seem almost endemic, yet these are problems that have been faced (and solved) by the safety-critical community for many years.

This tutorial will recount our experience in building high-grade secure systems using the CbyC approach developed by Praxis over the last 15 years.

Outline
Part I - Basics
Security basics - assumptions, threats, attacks, satan's computer Software correctness vs security

Part II - Correctness by Construction

  • CbyC principles and techniques
  • The role of formal languages and methods

Part III - Programming Languages and Static Analysis Language issues

  • Ada's position in all this
  • The SPARK approach to verification of security properties

o Basic protection from stupid mistakes
o Flow analysis and theorem proving
o Input data validation and injection attacks
o Domain and application-specific security properties

Part IV - Project examples

  • MULTOS CA
  • NSA Tokeneer

Why you should participate in this tutorial?
In recent years, software security has become a major issue. This tutorial will focus on how practices from the safety-critical industry can be used to address the engineering of secure systems. In particular, the tutorial will cover how Ada, SPARK, and static verification techniques can address the needs of secure systems development.

Presenter
The principal presenter will be Dr Roderick Chapman of Praxis High Integrity Systems.
Rodderick Chapman is a well-known conference speaker. He has presented papers, tutorials and workshops at many international events including STC, NSA HCSS, and ACM SIGAda. He was the opening key-note speaker at Ada Europe 2006.
Rod Chapman has been involved with the design of both safety- and security-critical software with Praxis for many years, including significant contributions to many of Praxis' key-note projects such as SHOLIS, MULTOS CA, Tokeneer, and the development of the SPARK language and verification tools. Rod is a chartered engineer and a Fellow of the BCS.


Synchronous design of embedded systems: the Esterel / Scade approach

Gerard Berry,

Esterel Technologies, France

(Friday June 29th, morning)

Abstract
This tutorial presents the synchronous design of embedded systems using the SCADE and Esterel Studio tools. The synchronous approach relies on a rigorous mathematical model of synchronous concurrent computation, which serves as a basis for the formal semantics of the languages. The tutorial mostly focuses on Scade, which is a graphical language. Scade models are defined by hierarchical block diagrams for continuous control and hierarchical state machines for discrete control, with unlimited nesting of both formalisms. The SCADE Suite tool provides model capture and sanity checking, visual simulation, model coverage analysis, C code generation, and formal verification. The tutorial will also briefly present Esterel Studio, a similar integrated development environment for the design, synthesis, and verification of hardware circuits and their software models.
Level: advanced

Heritage
the synchronous methodology and the associated tools are based on 25 years of research and more than 15 years of industrial applications.

Why you should participate in this tutorial?
SCADE is used by a large number of major companies to develop embedded safety-critical software for avionics, railway, automotive, and industry applications. Its C code generator is certified at highest level A of the DO-178B avionics norm, which makes it perfectly suited to certified software development. Esterel Studio is used by major hardware companies for the specification, synthesis, and verification of embedded hardware circuits together with their software models.

Presenter
Gerard Berry received his PhD in Mathematics in 1977. He is the father of the Esterel language. Before joining Esterel Technologies in January 2001, Mr. Berry was the Director of Research at Ecole des Mines de Paris (EMP), Director of the Applied Mathematics Center (CMA) of EMP, and co-head of the joint EMP/INRIA Meije project. His research activities include programming language designs, semantics and implementation, hardware synthesis and formal verification. Gerard Berry is a member of Académie des Sciences and Academia Europaea.


Building interoperable distributed applications with PolyORB

Thomas Quinot and Jérôme Hugues

AdaCore-ENST, France

(Friday June 29th, afternoon)

 Abstract
PolyORB is the reference implementation of the "schizophrenic" middleware architecture. This innovative architecture resolves middleware to middleware interoperability issues: it allows seamless integration of partitions in heterogeneous distribution environments (CORBA, DSA, web services) through the collaboration of multiple collocated personalities.
After presenting key concepts of distributed applications, we present two application fields of PolyORB:

  • as a CORBA implementation, using the iac IDL-to-Ada compiler, allowing integration in multi-language distributed applications;
  • as a supporting partition communication subsystem for the Ada Distributed Systems Annex (annex E), using the gnatdist partitioning tool.

We then present how to leverage the schizophrenic to take
advantage of both the CORBA and Ada DSA distribution
models. Specifically, we show how Ada components can interact seamlessly with components written in other languages through GIOP using the PolyORB-based DSA implementation and third-party CORBA implementations.
We then conclude by presenting other innovative aspects of PolyORB: integration of web services, security services, real-time.
PolyORB is developed as a joint effort by ENST, LIP6 and AdaCore, and supported by AdaCore. The PolyORB project is a member of the ObjectWeb consortium.

Why you should participate in this tutorial?
The intended audience for this tutorial is Ada application developers seeking to develop distributed applications. We specifically focus on distributed features of the Ada language, allowing seamless integration of distribution in the language itself, and on integration with industry standard CORBA components.

Presenters
Thomas Quinot has been involved with Ada and distributed systems since 1997. As part of his PhD research at Télécom Paris, he carried research on interoperability of heterogeneous distributed systems, and developed the Schizophrenic Middleware Architecture and its first implementation, PolyORB.

He contributed a reimplementation of the Ada 95 distributed systems annex for the GNAT compiler on top of the PolyORB components. He is now a senior engineer at AdaCore, where he is involved in the maintenance of GNAT and the industrial development of the PolyORB project.

Jérôme Hugues graduated from ENST in 2002, and got his PhD in 2005. He is now associate professor at the C/S department of the ENST. His research domain covers distributed systems, real-time systems and the use of modelling and formal methods applied to the engineering of complex systems. As part of his research activities, he was involved in the PolyORB project since its early stage in 2002, and since he became one of its lead architects. He uses PolyORB as a proof of concept of emerging techniques in distributed systems, and contributed many enhancements to its architecture and its internals:  better performance, determinism and compliance to standards, including CORBA and RT-CORBA. He also contributed to the formal verification of the inner core of PolyORB using Petri Nets. He also participates in the support and development of PolyORB in the context of an industrial partnership between AdaCore and the ENST.


Situational Method Engineering: Towards a Specific Method for Each System Development Project

Jolita Ralyté

University of Geneva, Switzerland

 (Friday June 29th, full day)

Abstract
Over the last decade Method Engineering, defined as the engineering discipline to design, construct and adapt methods and supportive tools, has emerged as the research and application area for using methods for software and information systems development. Because the engineering situation vary considerable from one system development project to another (different application domain, product features, licence form, stakeholders involved, team structure and various technological conditions), methods need to be adapted, configured or even designed from scratch to satisfy the specific situation of each project. Contributions in the field of Situational Method Engineering aim at providing techniques and tools allowing to construct project-specific methods instead of looking for universally applicable ones.
In this tutorial we will provide an overview of the main topics in the area of situational method engineering:

  • Method definition, description and meta-modelling,
  • Method engineering principles, techniques and tools,
  • Reusable method fragments, their selection and assembly,
  • Project situation assessment,
  • Selection, adaptation, configuration and construction of situation-specific methods,
  • Knowledge infrastructures, meta-case, and tool support.

Beside these topics, we will also discuss more recent work in the area of methods supporting interoperable ICT products development. Interoperability of enterprise applications and platforms will be analysed as a typical problem requiring situational method engineering.

Why you should participate in this tutorial?
The tutorial is designed for researchers, students and industrial practitioners dealing with software and information systems development. We invite researchers and Master students to increase their knowledge in the area of situational method engineering and to study techniques and principals for new methods construction. The tutorial is also a suitable introduction to situational method engineering for professionals. System analysts, designers, project managers and consultants are invited to learn how to evaluate their project situation and to tailor a suitable method, how to capitalise their knowledge, experience and best practices in the form or reusable method fragments and to create method knowledge repositories.

Presenters
Jolita Ralyté is currently a senior researcher and lecturer in the Department of Information Systems at the University of Geneva. She obtained a PhD in Computer Science from the University of Paris 1 – Sorbonne in 2001. The research areas of Dr. Ralyté include situational method engineering, requirement engineering, information systems evolution and interoperability and distributed information systems development. She has participated in diverse European research projects (TOOBIS, CREWS, INTEROP) and currently she is in charge of the International Method Engineering Task Group within the IFIP WG 8.1 and the task group TG6 dealing with methods and method engineering techniques supporting various systems interoperability issues within the European NoE INTEROP. Her work has been published in various international conferences (CAISE, ER, ICSP, ISD, I-ESA, IFIP WG8.1 EISIC’02) and international journals (RE, Knowledge-Based Systems). Dr Ralyté has been involved in the organisation of a number of international conferences and workshops (OOIS’03, EMSISE'03, Interop-ESA’05, SREP’05 and Doctoral Symposium at I-ESA’06) and co-edited a special issue of SPIP with revised best papers from SREP’05. Dr. Ralyté is a program chair of the IFIP WG 8.1 Working Conference ME07 to be held in Geneva in September 2007.