RvABS: Runtime Verification for ABS Product Lines (completed)

The RvABS-project is funded in 2012 as a bilateral Norwegian-German cooperation within the PPP-programme for collaborative research support scheme (``Projektbezogener Personenaustausch''). The cooperation is funded by the

You can find the sample project used in the ISOLA paper in SVN at http://svn.foldr.org/rCOS/ARV/model/CoCoME/. In addition, we have developed the necessary infrastructure to add the monitor-deltas to an ABS project based on an in-memory representation of the monitor. This requires two parts: first, an AspectJ-based Java project which augments the ABS frontend with an API to specify and to programmatically modify a model. The actual monitors for the CoCoME example are then specified and compiled in yet another project.

The compiled monitor can then be passed to the ABS compiler-frontend to generate the monitors on the fly, e.g. through

java -cp absfrontend.jar abs.backend.java.JavaBackend -v
     -weave=CoCoMeMonBaseProtocol CoCoME.abs Datatypes.abs

(The original ABS frontend is necessary, either from SVN [for HATS project members], or from the HATS website.)


We have also suggested to use similar code-manipulation techniques in our paper How useful are existing monitoring languages for securing Android apps? (to be presented at ATPS 2013), where we discuss specification languages for security monitors.

Tags: Runtime Verification, Software Product Lines, ABS, DAAD, HATS
Published May 31, 2012 5:37 PM - Last modified Aug. 7, 2013 10:06 AM