In this paper we introduce a new automata based test generation algorithm implemented in SPECPRO, our library for supporting analysis and development of formal requirements in cyber-physical systems. We consider specifications written in Linear Temporal Logic (LTL) from which we extract automatically trap properties representing the expected...
-
2019 (v1)PublicationUploaded on: March 27, 2023
-
2019 (v1)Publication
Property specification patterns (PSPs) have been proposed to ease the formalization of requirements, yet enable automated verification thereof. In particular, the internal consistency of specifications written with PSPs can be checked automatically with the use of, for example, linear temporal logic (LTL) satisfiability solvers. However, for...
Uploaded on: March 27, 2023