Enhancing system validation with behavioural types

The behaviour of systems is determined by their implementation in some form of source code. While behaviour itself is complex and its detailed semantics are hard to describe by means of lower level than a programming or specification language, the structure of dynamic input/output behaviour is limited by the system logic and fixed during operation in most cases. Certain aspects of system behavior can be captured by regular expressions that define the possible input/output behaviors of the system. A more refined kind of regular expression can be constructed that does not only represent I/O interleaving but also the location and type of every particular I/O event. This article describes the generation of such expressions and shows how they can be used to aid classic verification by testing, as well as in a criterion to assess the quality of given test case sets. Additionally, a method is sketched to falsify the behavioural identity of systems using the presented approach. Finally, a tool to apply the presented ideas in verification practice on MC68HC705J1A microcontroller programs is overviewed.