Logical verification of reactive software systems. - David Mark Jackson (1992)