Sciweavers

Share
SEKE
2005
Springer

Generating Properties for Runtime Monitoring from Software Specification Patterns

9 years 1 months ago
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.
Oscar Mondragon, Ann Q. Gates, Humberto Mendoza, O
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Where SEKE
Authors Oscar Mondragon, Ann Q. Gates, Humberto Mendoza, Oleg Sokolsky
Comments (0)
books