FORMSPEC


FORMSPEC - KIT125

Keywords: interface tools, real time, concurrent systems, verification, specification, technology transfer


Start Date: 31 October 94 / Duration: 36 months

[ participants / contact]


Objectivies and Approach

The main objective of this project is to study requirement and design specification notations for concurrent and real time systems. Existing as well as new specification notations will be investigated and formally defined with the aim of identifying notations suitable for use in industrial environments. Formal semantics using results from the ESPRIT EP8593 IDERS project, will be used to investigate the testing and validation of models expressed in the chosen notations. Advantages and disadvantages arising from restrictions imposed on the formal models by the chosen notations will be extensively investigated.

Progress and Results

Investigations on design notations for software analysis and design methodologies have already started, with the aim of complementing the results of the IDERS project. A design notation has been defined for the Hatley and Pirbhai methodology. The new notation has been given a formal semantics, and a prototype has been implemented based on IDERS' technology. The prototype has been validated on an industrial application with support from Alenia, one of the partners in the IDERS project. The prototype is now being used to study the impact of restrictions imposed by the front-end notation on the analysis of the kernel model.

Information Dissemination Activities and/or Exploitation

Results from the first part of the project have been exploited in the ESPRIT IDERS project. Related papers have been published in the proceedings of international conferences. The partners have validated the IDERS tool set by formally defining a design notation for the Hatley and Pirbhai methodology. Such a notation has already been used in a preliminary study with Alenia for the design of a Reply Processor and Channel Management for Radar Systems. The technical results are available as KIT Reports.


Coordinator

Dipartimento di Elettronica e Informazione
Politecnico di Milano., I

EU Partners

Politecnico di Milano, I
IFAD, DK

Non-EU Partners

LIFIA, AR

CONTACT POINT

Prof. Mauro Pezze
Tel: +39 2 239 93 523
Fax: +39 2 239 93 411
E-mail: pezze@elet.polimi.it


INCO synopses home page INCO cooperation index INCO keyword index
INCO acronym index INCO number index INCO Working Groups index
All
synopses home page all keywords index all acronyms index all numbers index

FORMSPEC - KIT125, May 1997


please address enquiries to the ESPRIT Information Desk

html version of synopsis by Nick Cook