Verifying complex systems

Many complex systems are built based on specifications defined in various formal languages, but many times the process of verifying their correctness is either long and tedious or impossible to be achieved due to the size of the problem. Such a specification language is utilised by a tool called FLAME and is based on a generalised state machine model. Although this language allows to define the components of the system in a very rigorous way and generates automatically coherent test sets, there are no explicit ways of verifying the validity of such systems. In many cases the simulation remains the last resort in validating the model through some partial executions. This project is looking into a coherent strategy of identifying properties of the system represented in FLAME and mechanisms to build effective ways of (partially) verifying these properties through adequate logics and model checking techniques.