Title: Design of a formal method for requirements analysis and
specification in ground transportation domain.

Keywords: requirement analysis, formal specification, components

Funding: Paris regional doctoral scholarship (approximately 1570€/month)
for a duration of 3 years.

Research Laboratory: Laboratory of Algorithmics, Complexity and Logic
(LACL), http://www.univ-paris12.fr/lacl/

PhD supervisor: Prof Regine Laleau
email : [log in to unmask]
Web page: http://www.univ-paris12.fr/lacl/laleau/

1 – Context
The proposed doctoral research is part of project TACOS
(http://tacos.loria.fr) funded by ANR’s 2006 SETIN programme. Its
objective is to build a component-based approach for specifying safe
systems, while describing requirements up to a formal specification.

The application domain is that of ground transportation, in particular
new types of vehicles called Cycabs are being put in self-service in
urban areas. The vehicles must be easy to use by a large public and
there is a real need to ensure their safety and reliability.

Computer systems found in Cycabs are both embedded and distributed. It
is necessary to express precisely their functional and non-functional
properties including availability and timed properties. The project is
motivated by:
- an increased user demand for certification and assurance of the trust
being put in such systems,
- the role of a rigorous requirements expression, needed to build
trustable systems meeting the needs and properties of their environment.

Project TACOS is composed of three parts:
- Expression of non-functional properties in the requirements
engineering phase.
- Specification of a trustable components assembly. The approach must
deal with specification of components, assembly of components and
verification of their combination.
- Traceability between requirements expression and specification of
components.

The proposed thesis work deals mainly with the first part while taking
into account the needs of traceability (part 3).

2 – Objectives
The framework of the thesis is requirement engineering, which plays a
fundamental role in the system development life cycle. Existing research
work has shown that RE needs first to define the objectives of the
future system and to consider also properties of the system environment.
Objectives, system and domain properties are the basic elements to build
a model of the future system.
The first thesis objective is to obtain a generic requirements model
applicable to all kinds of Cycab systems. Both functional and
non-functional requirements have to be considered, and more specifically
security requirements have to be precisely identified. Domain properties
representing static and dynamic constraints will be identified and
linked to relevant goals. However these elements need to be formalized,
in order to check that the right system is built. The second objective
of the thesis is to elaborate a method, adapted to the ground
transportation domain, that allows environment, functional and
non-functional requirements to be formalized. The method will be
component-based in order to be combined with the component-based
approach chosen in the TACOS project. The formal language will be that
of the B method. This method has been and continues to be used in the
design of complex and industrial applications such as Line 14 of the
parisian underground or smartcard. It is supported not only by
commercial tools (like Atelier B) but also by an open tool B4free
(http://www.b4free.com/).
The last objective is to develop an open tool associated with the
method. It will be a combination of existing open tools such as B4free
and StarUML (http://staruml.sourceforge.net/en/) for requirements analysis.

This work will be conducted at LACL close to Paris
(www.univ-paris12.fr/lacl) in collaboration with partner research labs:
LORIA at Nancy, LIFC at Besançon and LAMIH at Valenciennes.

-- 

Regine LALEAU, professeur

Universite Paris 12, laboratoire LACL
et
IUT Fontainebleau, Departement informatique
Route forestiere Hurtault
77300 Fontainebleau, France
Tel : (+33) (0) 1 60 74 68 40, secr. (+33) (0) 1 60 74 68 02
Fax : (+33) (0) 1 60 74 68 28

Tel  (nouveau numero) : (+33) (0) 6 67 77 44 80

http://www.univ-paris12.fr/lacl/laleau/