forked from runtimeverification/llvmmop
-
Notifications
You must be signed in to change notification settings - Fork 0
MOP framework for LLVM
License
isabella232/llvmmop
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Folders and files
Name | Name | Last commit message | Last commit date | |
---|---|---|---|---|
Repository files navigation
JavaMOP 2.3.1 README ==1. Overview== Monitoring-Oriented Programming, abbreviated MOP, is a software development and analysis framework aiming at reducing the gap between formal specification and implementation by allowing them together to form a system. In MOP, runtime monitoring is supported and encouraged as a fundamental principle for building reliable software: monitors are automatically synthesized from specified properties and integrated into the original system to check its dynamic behaviors during execution. When a specification is violated or validated at runtime, user-defined actions will be triggered, which can be any code from information logging to runtime recovery. One can understand MOP from at least three perspectives: as a discipline allowing one to improve safety, reliability and dependability of a system by monitoring its requirements against its implementation at runtime; as an extension of programming languages with logics (one can add logical statements anywhere in the program, referring to past or future states); and as a lightweight formal method. JavaMOP is an instance of MOP for Java. For more information, refer to the following URL: javamop.googlecode.com ==2. Installation== For detailed installation instructions, please see the INSTALL file. As the tool is still under active development, it is recommended that you install JavaMOP directly from the svn repository and update it regularly using svn up from the base directory to benefit of the latest fixes and features. ==3. Usage== =3.1 Linux and Mac (POSIX) If you want to use the Logic Repository Server provided by UIUC, use the -remote option when using the 'javamop' script. If you want to use the Logic Repository included in this package, use the -local option when using the 'javamop' script. Using the remote repository is the preferred method for computers with viable Internet connections as it allows us to collect usage statistics used to improve JavaMOP. The 'javamop' script has the following usage: Usage) javamop [-v] [-d <target directory>] <specification file or dir> -v option is verbose mode -d option is used to specify the target directory where the resulting aspect code will be saved. Specification files must have The .mop file extension. Example) javamop -d examples/FSM/ examples/FSM/HasNext.mop For more options, type 'javamop' or 'javamop -h' =3.2 Windows If you want to use the Logic Repository server provided by UIUC, use -remote option when using the script 'javamop.bat' If you want to use the Logic Repository included in this package, use -local option when using the script 'javamop.bat' The script, 'javamop.bat' has the following usage. Usage) javamop.bat [-v] [-d <target directory>] <specification file or dir> The -v option is used to specify verbose mode. The -d option is used to specify the target directory where the resulting aspect code will be saved. Specification files must have The .mop file extension. Example) javamop.bat -d examples\FSM examples\FSM\HasNext.mop For more options, type 'javamop.bat' or 'javamop.bat -h' ==4. Additional Features of the JavaMOP Distribution== =4.1 Executing a Monitored Program When you execute a monitored program, you need to include the AspectJ library and JavaMOP Runtime Library in your class path. The JavaMOP Runtime Library is provided in this package in the javamop2.3/lib directory. A typical value of this is: In Windows, c:\javamop2.3\lib\javamoprt.jar In Linux and Mac, ~/javamop2.3/lib/javamoprt.jar Add this to the left end of the "CLASSPATH" followed by ";" (in Windows) or ":" (in Linux and Mac). For more information, refer to Section 5 from the following URL http://java.sun.com/j2se/1.4.2/install-windows.html =4.2 Running the Logic Repository Tool JavaMOP uses the Logic Repository automatically. Therefore, you do not need to invoke the Logic Repository explicitly. JavaMOP will connect to the Logic Repository automatically and retrieve a monitor for the given specification. However, it is possible to use the Logic Repository directly for other uses. To use the LogicRepository, type 'logicrepository' in Linux and Mac, 'logicrepository.bat' in Windows. And provide input through the standard input. For the XML syntax of input, refer to the following pages: http://fsl.cs.uiuc.edu/index.php/Special:LogicRepository2.3 The resulting monitoring code is piped to standard output, in XML format. =5. Contact Information We welcome your interest in JavaMOP. Your feedback, comments and bug reports are highly appreciated. Please feel free to contact us by sending email to mop@cs.uiuc.edu. Bugs and feature requests may be submitted at the project website at javamop.googlecode.com.
About
MOP framework for LLVM
Resources
License
Code of conduct
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published
Languages
- Java 99.6%
- Other 0.4%