Monitoring Method Call Sequences Using Annotations

Behrooz Nobakht, Marcello M. Bonsangue, Frank S. de Boer, Stijn de Gouw

Research output: Chapter in Book/Report/Conference proceedingConference Article in proceedingAcademicpeer-review


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 languageEnglish
Title of host publicationFormal Aspects of Component Software
Subtitle of host publication7th International Workshop, FACS 2010, Guimarães, Portugal, October 14-16, 2010, Revised Selected Papers
EditorsLuís Soares Barbosa , Markus Lumpe
Number of pages18
ISBN (Electronic)978-3-642-27269-1
ISBN (Print)978-3-642-27268-4
Publication statusPublished - 2010
Externally publishedYes
EventFormal 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 201016 Oct 2010


ConferenceFormal Aspects of Component Software FACS 2010
Abbreviated titleFACS 2010
Internet address


Dive into the research topics of 'Monitoring Method Call Sequences Using Annotations'. Together they form a unique fingerprint.

Cite this