Title

Temporaljmlc: A Jml Runtime Assertion Checker Extension For Specification And Checking Of Temporal Properties

Keywords

Java Modeling Language; Runtime assertion checking; Specification patterns; Temporal specification; Temporaljmlc

Abstract

Most mainstream specification languages primarily deal with a program's functional behavior. However, for many common problems, besides the system's functionality, it is necessary to be able to express its temporal properties, such as the necessity of calling methods in a certain order. We have developed temporaljmlc, a tool that performs runtime assertion checking of temporal properties specified in an extension of the Java Modeling Language (JML). The benefit of temporaljmlc is that it allows succinct specification of temporal properties that would otherwise be tedious and difficult to specify. © 2010 IEEE.

Publication Date

12-28-2010

Publication Title

Proceedings - Software Engineering and Formal Methods, SEFM 2010

Number of Pages

63-72

Document Type

Article; Proceedings Paper

Personal Identifier

scopus

DOI Link

https://doi.org/10.1109/SEFM.2010.15

Socpus ID

78650431910 (Scopus)

Source API URL

https://api.elsevier.com/content/abstract/scopus_id/78650431910

This document is currently not available here.

Share

COinS