Java-MaC: A Run-Time Assurance Approach for Java Programs. We describe Java-MaC, a prototype implementation of the Monitoring and Checking (MaC) architecture for Java programs. The MaC architecture provides assurance that the target program is running correctly with respect to a formal requirements specification by monitoring and checking the execution of the target program at run-time. MaC bridges the gap between formal verification, which ensures the correctness of a design rather than an implementation, and testing, which does not provide formal guarantees about the correctness of the system. Use of formal requirement specifications in run-time monitoring and checking is the salient aspect of the MaC architecture. MaC is a lightweight formal method solution which works as a viable complement to the current heavyweight formal methods. In addition, analysis processes of the architecture including instrumentation of the target program, monitoring, and checking are performed fully automatically without human direction, which increases the accuracy of the analysis. Another important feature of the architecture is the clear separation between monitoring implementation-dependent low-level behaviors and checking high-level behaviors, which allows the reuse of a high-level requirement specification even when the target program implementation changes. Furthermore, this separation makes the architecture modular and allows the flexibility of incorporating third party tools into the architecture. The paper presents an overview of the MaC architecture and a prototype implementation Java-MaC.
Keywords for this software
References in zbMATH (referenced in 11 articles , 1 standard article )
Showing results 1 to 11 of 11.
- Francalanza, Adrian: A theory of monitors (2021)
- Natarajan, Aravind; Chauhan, Himanshu; Mittal, Neeraj; Garg, Vijay K.: Efficient abstraction algorithms for predicate detection (2017)
- Francalanza, Adrian: A theory of monitors (extended abstract) (2016)
- Bonakdarpour, Borzoo; Navabpour, Samaneh; Fischmeister, Sebastian: Time-triggered runtime verification (2013)
- Sokolsky, Oleg (ed.); Roşu, Grigore (ed.): Introduction to the special issue on runtime verification (2012)
- Aktug, Irem; Dam, Mads; Gurov, Dilian: Provably correct runtime monitoring (2009)
- Chen, Feng; Roşu, Grigore: Java-MOP: A monitoring oriented programming environment for Java (2005)
- d’Amorim, Marcelo; Roşu, Grigore: Efficient monitoring of (\omega)-languages (2005)
- Kim, MoonZoo; Viswanathan, Mahesh; Kannan, Sampath; Lee, Insup; Sokolsky, Oleg: Java-MaC: A run-time assurance approach for Java programs (2004)
- Sen, Koushik; Roşu, Grigore; Agha, Gul: Online efficient predictive safety analysis of multithreaded programs (2004)
- Sen, Koushik; Roşu, Grigore; Agha, Gul: Generating optimal linear temporal logic monitors by coinduction. (2003)