Requirements formalization and validation for a telecommunication equipment protection switcher

Using 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 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