R & D Summary

    BeSSY - Formally Specifying the Behaviours of Software Components

In computer science, formal methods refer to a category of mathematically-based techniques used to describe (specify), develop and verify software. The generally accepted advantage of formal methods is un-ambiguity in the description which can then be tested and verified. This makes formal methods a very useful means of asynchronous technical communication (handing over software codes from developers to maintainers).

However, the acceptance and use of formal methods has been slow over the last 2 decades due to 2 main reasons. Firstly, the use of mathematical notations is often cited as reason for slow uptake of formal methods. Reading notations and constructing mathematical structures are often unacceptable to many people, including software developers. At the same time, formatting mathematical notations on computer is not exactly a pleasure. Secondly, formal methods today is rather incompatible with software engineering process. The resulting specification has not much use in itself - unable to be transformed into code structures and so on. Hence, formal specification writing is often seen as a mental masturbation for academics (Bowen and Hinchey 1995). Despite so, I believe that formal specification has its uses.

I am also interested to teach my students some form of formal description skills so that they can explain a system concisely. However, the level of mathematics required must be simple and intuitive enough to be taught and understood. A description that is difficult to understand is nothing more than pure mental stimulation.

BeSSY (Behavioural Specification System) attempts to use no more than high-school mathematics (arithmetic, sets theory, functions, and Boolean algebra) as a basis to describe software systems. Functions and logic (in the form of boolean algebra) is an important aspect of computer programming; hence, is a bridge to convert a specification to skeletal source codes.