Testing dynamic systems from modal specifications

Among other validation and verification techniques, testing is a widely used method for ensuring a certain quality to software systems. When the implementation of the system is not known, it can be tested with respect to a (formal) specification. Classically, the specifications used to test functional programs are logical while those used for dynamic systems are transition systems. I will show here how the logical approach, when dealing with modal logics, can be used for testing dynamic systems, viewed as coalgebras.

hosted by