A gentle introduction to specification engineering using a case study in telecommunications

Software development based on formal methods is the only way to provably correct software. Therefore a method for the development of complex systems in intuitive steps is needed. A suitable solution is the transformational approach where verified semantics-preserving transformation rules are used to come from a first verified specification to the desired system. A problem is that for most industrial applications the system development never terminates because requirements change and new functionalities have to be added to the system. This paper describes a new approach for the development of extensible specifications in small intuitive steps. New transformation rules are introduced that guarantee that intermediate results of development can be used for further steps.