GENERATING PROPERTIES FOR RUNTIME MONITORING FROM SOFTWARE SPECIFICATION PATTERNS

摘要

This paper presents an approach to support run-time verification of software systems that combines two existing tools, Prospec and Java-MaC, into a single framework. Prospec can be used to clarify natural language specifications for sequential, concurrent, and nondeterministic behavior. In addition, Prospec assists the user in reading, writing, and understanding formal specifications through the use of property patterns and visual abstractions. Prospec automatically generates specifications written in Future Interval Logic (FIL). Java-MaC monitors Java programs at runtime to ensure adherence to a set of formally specified properties. Safety properties of a program are specified in the formal language Meta-Event Definition Language (MEDL). Java-MaC generates runtime components from specifications. The components are used to instrument the target program and determine whether the execution of the program violates any of the safety properties. This paper describes an algorithm for translating FIL formulas into MEDL formulas. It provides the transformation rules used by this algorithm, and it demonstrates the general correctness of the translation.