Graphical Input Sketches for Producing Formalised Behavioural Requirements
Peter J. Funk, Dave Robertson · 1998
. Formal methods are usually intended to include all the details of the final system in the specification, with the aim of proving that it possesses certain mathematical properties. Telecommunications services are large and complex, making detailed formal specification impractical with current technology [Mataga & Zave, 1993]. Fortunately, the behaviour of the services provided to telephone users is often simple enough to sketch and much of the complexity stems from details of the implementation of services. The principal characteristics of a service can be approximated by simple varieties of logic, even though the services themselves cannot usually be formalised. We address the problem of determining these services, from a library of services accompanied by their behavioural approximations, which might be appropriate for re-use, by using graphical input examples to sketch the behaviour desired and a case-based approach to identify behaviourally similar telecommunications se...