Abstract
In this paper we introduce JMSeq, a Java-based tool for the specification and runtime verification via monitoring of sequences of possibly nested method calls. JMSeq provides a simple but expressive way to specify the sequential execution of a Java program using code annotations via user-given sequences of methods calls. Similar to many monitoring-oriented environments, verification in JMSeq is done at run-time, but differently from all other approaches based on aspect-oriented programming, JMSeq does not use code instrumentation, and therefore is suitable for component-based software verification.
| Original language | English |
|---|---|
| Title of host publication | Formal Aspects of Component Software |
| Subtitle of host publication | 7th International Workshop, FACS 2010, Guimarães, Portugal, October 14-16, 2010, Revised Selected Papers |
| Editors | Luís Soares Barbosa , Markus Lumpe |
| Publisher | Springer |
| Pages | 53-70 |
| Number of pages | 18 |
| ISBN (Electronic) | 978-3-642-27269-1 |
| ISBN (Print) | 978-3-642-27268-4 |
| DOIs | |
| Publication status | Published - 2010 |
| Externally published | Yes |
| Event | Formal Aspects of Component Software FACS 2010: 7th International Workshop on Formal Aspects of Component Software - Hotel de Guimarães, Guimarães, Portugal Duration: 14 Oct 2010 → 16 Oct 2010 http://www4.di.uminho.pt/facs2010/ |
Conference
| Conference | Formal Aspects of Component Software FACS 2010 |
|---|---|
| Abbreviated title | FACS 2010 |
| Country/Territory | Portugal |
| City | Guimarães |
| Period | 14/10/10 → 16/10/10 |
| Internet address |