Generating Properties for Runtime Monitoring from Software Specification Patterns

The 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, the tool assists the user in reading, writing, and understanding formal specifications through the use of property patterns and bstractions. Currently, Prospec automatically generates a specification written in Future Interval Logic (FIL). The goal is to automate the generation of MEDL formulas that can be used by the Java-MaC tool to check run-time compliance of system execution to properties. The paper describes the mapping that translates FIL formulas into MEDL formulas and demonstrates its correctness.

• Type: Conference
• Year: 2005
• Where: SEKE
• Authors: Oscar Mondragon, Ann Q. Gates, Humberto Mendoza, Oleg Sokolsky
• Keywords: MEDL Formulas, Natural Language Specifications, Run-time Verification, SEKE 2005