Conference 

5th IEEE International Symposium on
``High Assurance Systems Engineering'' (HASE),
Nov. 15-17, 2000, Albuquerque, New Mexico, USA



Paper Title

Requirements Formalization and Validation for a 
Telecommunication Equipment Protection Switcher




Authors, Affiliations

Michele Cecconi
SIEMENS ICN SPA, 
Localita` Boschetto, 
I-67100 L'Aquila, ITALY
email: michele.cecconi@icn.siemens.it


Enrico Tronci
Area Informatica
Universita` di L'Aquila
Coppito I-67100 L'Aquila, ITALY
email: tronci@univaq.it 
url:  http://univaq.it/$\sim$tronci



Abstract

Using {\em formal methods}, namely model checking, 
we can automatically verify a formal model of the requirements
against given properties.
This allows us to detect errors early in the design process,
thus decreasing development cost and time to market.
However to modify a well established design process
to introduce formal methods is not easy.


We present a case study exploring the possibility of
replacing informal functional  specifications with formal ones
in the design process of telecommunication 
{\em Equipment Protection Switchers} (EPSs).

Our finding is that for EPSs the time effort
to write formal specs from informal requirements is comparable
with that for writing informal functional specs from informal requirements.
This suggests that for EPSs replacing 
informal functional specs in the design process
with formal specs can be done
without suffering 
delays due to the formalization activity.



Keywords

Model Checking, Formal Methods, Automatic Validation,
Telecommunication Systems, Reactive Systems, Embedded Systems,
Finite State Systems,  Binary Decision Diagrams.