GENERATING PROPERTIES FOR RUNTIME MONITORING FROM SOFTWARE SPECIFICATION PATTERNS
Abstract
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.
References
- Int. J. SEKE 14(1), 21 (2004), DOI: 10.1142/S0218194004001567. Google Scholar
-
O. Mondragon , A. Q. Gates and S. Roach , Prospec: Support for elicitation and formal specification of software properties , Proc. Runtime Verification Workshop ,ENTCS 89 , eds.O. Sokolsky and M. Viswanathan ( 2003 ) . Google Scholar M. B. Dwyer , G. S. Avrunin and J. C. Corbett , Property specification patterns for finite-state verification, Proc. 2nd Workshop on Formal Methods in Software Practice pp. 7–15. Google ScholarM. Kim , Java-MaC: a run-time assurance tool for Java programs, Proc. Runtime Verification Workshop, eds.K. Havelund and G. Rosu (2001) pp. 97–104. Google Scholar- , High Integrity Software, ed.
Bhattacharya (Academic Press, 2001) pp. 115–135. Crossref, Google Scholar - O. Mondragon, Elucidation and Specification of Software Properties through Patterns and Composite Propositions to Support Formal Verification Techniques, PhD Dissertation, Computer Science Department, University of Texas at El Paso, May 2004 . Google Scholar
- Theoretical Computer Science 166(1–2), 1 (1996), DOI: 10.1016/0304-3975(95)00254-5. Crossref, Web of Science, Google Scholar
- H. Mendoza, FIL to MEDL: A Translation Tool for the Future Interval Logic to Meta Event Definition Language, Masters Project Report, Computer Science Department, University of Texas at El Paso, April 2005 . Google Scholar
K. Havelund and G. Rosu , Monitoring programs using rewriting, Proc. Int. Conf. ASE 01 pp. 135–143. Google ScholarK. Havelund and G. Rosu , Synthesizing monitors for safety properties,LNCS 2280 pp. 442–456. Google ScholarR. Smith , PROPEL: An approach supporting property elucidation, Proc. ICSE pp. 11–21. Google ScholarS. Salamah , Verifying pattern-generated LTL formulas: A case study, 12th Int. SPIN Workshop,LNCS 3639 (Springer) pp. 200–220. Google Scholar- IEEE Trans. SE 23(5), 279 (1997), DOI: 10.1109/32.588521. Crossref, Web of Science, Google Scholar
