Behavioural validation of software engineering artefacts

Software engineering artefacts that define behaviour tend to be of a fragmented nature in order to facilitate their construction, modification, and modular reasoning (e.g. modular code, pre/post-conditions specifications). However, fragmentation makes the validation of global behaviour difficult. Typically synthesis techniques that yield global representations of large or infinite states are used in combination with simulation or partial explorations, techniques which necessarily lose the global view of system behaviour. I am working on the development of abstraction-for-validation techniques that automatically produce finite state abstractions that are sufficiently small to support validating the emergent behaviour of a fragmented description "at a glance".