Course 6 – 11 November 2019 Adrian Iftene [email protected]
Recapitulation course 6
◦ AOP
AOP
◦ Profiler
◦ Tracing
◦ Pooling
◦ PostSharp
◦ Spring Framework
Runtime Verification
◦ Model Checking
MOP
◦ Java MOP
2
Concern - a feature point, or requirement
Crosscutting concern - a feature point that cannot be encapsulated in one class
Aspect - the code for new functionality
Join Points - a specific point in the execution of the
program (method calls, constructor invocations, exception handlers)
Pointcuts - a structure and syntax for selecting join points
Advice - code to be executed when a join point is reached
Introductions (Inter-type declaration) - the ability of aspect oriented programs to alter existing program
structure (adding members to existing classes, adding methods, etc.)
4
A crosscutting concern is a concern that needs to be applied in many different compilation
modules
◦ “All exceptions must be logged”
◦ “Capture all sql statements produced by the application”
◦ “Cache all data that is rarely changed”
◦ “Record all changes to the account for historical purposes”
◦ “Timing, authentication, and persistence”
Java Code Aspect
public class Student { public aspect StudentAspect {
ajc compiling
public class WeavedStudent {
6
pointcut name([parameters]): designator(ajoinpoint);
Designators: execution, call, initialization, handler, this, args, target
Advice:
type ([parameters]) : joinpointid (param list) { … }
Type can be: before, after (returning, throwing) and around
call (* * Student.* (*))
call (* * . (*))
call (* * . (..))
call (* * Student+.* (*))
call (public void Student+(. .) throws Exception+)
8
How do you explain the result below?
10
12
14
+ 41771 1322291826194 void student.Student.setName(String) - 41771 1322291826196 void student.Student.setName(String) + 41771 1322291826196 void student.Student.setGrade(int)
+ 41771 1322291826196 StringBuilder java.lang.StringBuilder.append(int) - 41771 1322291826196 StringBuilder java.lang.StringBuilder.append(int) + 41771 1322291826196 String java.lang.StringBuilder.toString()
- 41771 1322291826196 String java.lang.StringBuilder.toString() + 41771 1322291826196 void java.io.PrintStream.println(String) - 41771 1322291826196 void java.io.PrintStream.println(String) - 41771 1322291826199 void student.Student.setGrade(int) + 41771 1322291826199 void student.Student.setMaxGrade() + 41771 1322291826199 void student.Student.setGrade(int)
+ 41771 1322291826199 StringBuilder java.lang.StringBuilder.append(int) - 41771 1322291826199 StringBuilder java.lang.StringBuilder.append(int) + 41771 1322291826199 String java.lang.StringBuilder.toString()
- 41771 1322291826199 String java.lang.StringBuilder.toString() + 41771 1322291826199 void java.io.PrintStream.println(String)
16
18
With PostSharp, you can easily write and apply custom attributes that add new behaviors to your code - tracing, thread management, exception handling, data binding, and much more
Write an Aspect
20
Just annotate relevant methods with the aspect:
You can also apply the aspects to many classes and methods in a single line, without even touching the source code of these classes.
An open source application framework for Java
The first version (Rod Johnson) was released with the publication of book Expert One-on-One J2EE Design and Development in October 2002
The framework was first released under the Apache 2.0 license in June 2003. The current version is 5.0.0 (http://projects.spring.io/spring-framework/)
The core features can be used by any Java application, but there are extensions for building web applications on top of the Java EE platform
It is very popular in the Java community as an
alternative to, replacement for, or even addition to the Enterprise JavaBean (EJB) model
22
Inversion of Control container
Aspect-oriented programming
Data access
Transaction management
Model-view-controller
Remote Access framework
Convention-over-configuration
Batch processing
Authentication and authorization
Remote Management
Messaging
Testing
24
Join point: a point during the execution of a program
Introduction: declaring additional methods or fields on behalf of a type
Target object: object being advised by one or more aspects
AOP proxy: an object created by the AOP framework in order to implement the aspect contracts
A point during the execution of a program, such as the execution of a method or the handling of an
exception
A set of join points is described as a pointcut
In Spring AOP, a join point always represents a method execution
A locus of points where execution will happen
26
Declaring additional methods or fields on behalf of a type
Spring AOP allows you to introduce new interfaces
(and a corresponding implementation) to any advised object
For example, you could use an introduction to make a bean implement an IsModified interface, to simplify caching
An introduction is known as an inter-type declaration in the AspectJ community
Object being advised by one or more aspects
Also referred to as the advised object
Since Spring AOP is implemented
using runtime proxies, this object will always be a proxied object
28
An object created by the AOP framework in order to implement the aspect contracts (advise method
executions and so on)
For example, in the Spring Framework, an AOP proxy will be a JDK dynamic proxy or a CGLIB proxy
Recapitulation course 6
◦ AOP
AOP
◦ Profiler
◦ Tracing
◦ Pooling
◦ PostSharp
◦ Spring Framework
Runtime Verification
◦ Model Checking
MOP
◦ Java MOP
30
Verification: comprises all techniques for showing that a system satisfies its specification
Runtime Verification: Runtime verification deals with those techniques that allow checking
whether a system under scrutiny satisfies or violates a given safety property
It aims to be lightweight verification technique
complementing verification techniques such as
model checking or testing
Run of systems produces lots of observations
What we can verify?
◦ Is it correct?
◦ Does it have the necessary performance, reliability, scalability, security?
◦ Output is correct accordingly with the input?
◦ The hardware components are used properly?
◦ Usability is respected?
Each of these questions is a property that
needs to be checked
32
Runtime verification (RV) is concerned with
monitoring and analysis of software or hardware system executions
Involves three basic techniques:
◦ theorem proving (using mathematics)
◦ model checking (with automated verification)
◦ Testing
The field is referred as runtime verification,
runtime monitoring, runtime checking, runtime reflection, runtime analysis, dynamic analysis,
symbolic dynamic analysis, trace analysis, log file
analysis
A “software failure” is a deviation between
observed behavior and required behavior of a software system
A “fault” is identified by the deviation of current status in compared with expected state of the system
An “error” is a mistake that belongs to programmer error resulting in a “fault” and possibly a “software failure”
Model Checking is an automatic technique for verifying finite-state reactive systems
Model Checking is a method for formally verifying finite-state concurrent systems
Problem: Given a model of a system, test
automatically whether this model meets a given specification
34
An important class of model checking methods are specified using temporal logic formulas
Temporal logic – a formula is not true or false in a static way in a model
Temporal logic models contain several states and a formula can be true in some states and false in others
The model is a transitional system and properties are temporal formulas
Now Future time
Past time
36
In our case, we have hardware or software systems, and the specification contains safety requirements
(i.e. the absence of deadlocks and the identification of critical states that can cause the system to crash)
Checking the system involves:
◦ Using a descriptive language for the model checker
◦ Encode concerned properties using the model checker language specification
◦ Running the model checker with: model and formulas as input
38
Direct observation for simple traces of events
◦ Programmer, tester on a small data volume
◦ Comparison between expected and obtained
Custom checker
◦ Start from simple scripts (Perl, Python, Java script)
◦ We can check the correspondence between values, if the values belonging to a domain, the QoS
◦ We can use monitors, logs, aspects
Checker for a suitable property specification language
◦ Can be formal: use the formal semantics for checking the satisfaction
Runtime verification concerns only detect violations or compliance with fairness properties
The execution of a software system (“run”) is
considered as a possible infinite sequence of states of the system
States can be: variable assignments or sequences of actions issued and performed by a system
Formally, an execution is considered as a possible infinite word or trace
Execution of a system is a finite prefix of that run or a
finite trace 40
Checking the execution of a system in relation to a fairness property is the responsibility of the monitor
The basic functionality of such a monitor is to decide if the current execution satisfies a property
We can extrapolate and say that check at runtime, in terms of mathematical and formal attempts to develop techniques able to provide a response regarding the inclusion of a word (trace) in a language (set of states of a system)
Online monitoring - involves using a monitor to check the current execution of a system
Offline monitoring - involves using a monitor for a finite set of executions recorded
In terms of runtime verification, monitors are automatically generated from a high-level
specification
42
The concept of “safety property” trying to capture a behavioral property related to the execution trace
Basic characteristic is given by the fact that once violated (property), it can not be satisfied
Safety properties can be applied over finite or
infinite traces
A monitor is a specialized automated, without terminal states
Ḿ =(S, s
0, M: S x ∑ → S)
Properties of a monitor
◦ Ĺ*( Ḿ ) = { w ϵ ∑* | M (s0,w) ↓}
◦ Ĺ (Ḿ ) = { u ϵ ∑ | M (s0,w) ↓} for all w ϵ prefixes(u)}
◦ Ĺ*, (Ḿ ) = Ĺ*( Ḿ ) Ĺ ( Ḿ )
44
General idea of running for a monitor
◦ Specialized automated will be triggered by events generated by the system that we observe
◦ For each new event observed, the monitor moves from current state into another state
◦ If transition function is undefined for the current state and for the current event => monitored
property is violated at that point
46
The observation mechanism extracts property relevant and filtered system states at designated points, e.g., when property-specific events happen
The verification mechanism checks the obtained
abstract trace against the (monitor corresponding to the) property and triggers desired actions in case of violations or validations
48
The first component (the header) will include information about monitoring, generation and
integration. Can be added information regarding the purpose and logic used to define properties for
monitoring
In the second part (body) monitored properties are declared, these formulas will be associated with
certain logic plug-ins, according to the used formal semantic
Last part (handler) is the code declared by
programmer for cases when property is respected or violated
50
Example: for global property “always (x > 0)”
Observation mechanism – is related to updates of the variable x and the relevant state information (or
snapshot) to extract is the value of x => a sequence of values of x
Verification mechanism - checks whether the value of x is larger than zero
=> Observation and verification are independent
/*@
scope = class logic = ERE
{
[static int counter = 0; int writes = 0;]
event open : end(call(* open(..))) {writes = 0;};
event write : end(call(* write(..))) {writes ++;} ; event close : end(call(* close(..)));
formula : (open write+ close)*
}
violation handler{ @RESET; }
validation handler{ synchronized(getClass()){
File.log((++counter) + ":" + writes); } }
@*/
MOP specification for file profiling
52
/*@
scope = global logic = ERE
SafeEnum (Vector v, Enumeration+ e) { [String location = "";]
event create<v,e>: end(call(Enumeration+.new(v,..))) with (e);
event updatesource<v>: end(call(* v.add*(..))) \/
end(call(* v.remove*(..))) \/ ...
{location = @LOC;}
event next<e>: begin(call(* e.nextElement()));
formula : create next* updatesource+ next
}
validation handler { System.out.println("Vector updated at "
+ @MONITOR.location); }
@*/
MOP specification for safe enumeration
Authentication before use
Execution 1, correct
authenticate
begin end
use
begin end
Execution 2, incorrect
54
class Resource { /*@
class-scoped SafeUse() {
event authenticate : after(exec(* authenticate())) event use : before(exec(* access()))
ptltl : use -> <*> authenticate }
@*/
void authenticate() {...}
void access() {...}
...
}
Enforce authentication before use
Execution 1, correct
authenticate
begin end
use
begin end
Execution 2, incorrect but corrected
Call
authenticate()
56
Enforce authentication before use
class Resource { /*@
class-scoped SafeUse() {
event authenticate : after(exec(* authenticate())) event use : before(exec(* access()))
ptltl : use -> <*> authenticate
violation { @this.authenticate(); } }
@*/
void authenticate() {...}
void access() {...}
...
}
JavaMOP is an MOP development tool for Java
JavaMOP follows a client-server architecture
◦ The client part includes the interface modules and the JavaMOP specification processor
◦ The server part contains a message dispatcher and logic-plugins for Java
The specification processor employs AspectJ for monitor integration => JavaMOP translates
outputs of logic-plugins into AspectJ code
58
Vector v=new Vector();
v.add(new Integer(10));
Iterator i =v.iterator();
v.add(new Integer(20));
System.out.println(i.next());
JVM: ConcurentModificationException
Fail-fast iterator
60
package mop;
import java.io.*;
import java.util.*;
HasNext(Iterator i) {
event hasnext after(Iterator i) : call(* Iterator.hasNext()) && target(i) {}
event next before(Iterator i) : call(* Iterator.next()) && target(i) {}
ptltl : next implies (*) hasnext
@violation {
System.out.println("next called without hasNext!");
} }
62
Map SafeEnum_v_map = makeMap();
pointcut SafeEnum_updatesource0(Vector v) : call(* Vector.add*(..))&&
target(v);
after (Vector v) : SafeEnum_updatesource0(v) { Map m = SafeEnum_v_map;
Object obj = null;
obj = m.get(v);
if (obj != null){
Iterator monitors = ((List)obj).iterator();
while (monitors.hasNext()) {
SafeEnumMonitor monitor=(SafeEnumMonitor)monitors.next();
monitor.updatesource(v);
if (monitor.suceeded()) {//validation handler
} }//end of while }//end of if
}
1) On-line:
http://fsl.cs.illinois.edu/index.php/JavaMOP4 http://fsl.cs.illinois.edu/index.php/MOP
http://www.kframework.org/tool/run/javamop Steps:
a) Specify the monitor + run it
b) The result (a new class and an aspect (the monitor)) must be added in an AspectJ project
c) At AspectJ project must be added a new test class d) Run the project and it must work
2) Off-line: At command line:
ajc -1.5 -cp <AspectJ runtime library>:<Apache Commons Collection library> -input <the base program root folder>
64
Implement a monitor for your project (max 2
persons)
66
A look at aspect-oriented programming:
http://www.ibm.com/developerworks/rational/library/2782.html
Implementing caching with AspectJ:
http://www.aspectprogrammer.org/blogs/adrian/2004/06/implementing_ca.html
Debugging Class Loading with AOP: http://www.cubeia.com/index.php/articles/63- debug-class-loading
Using AOP in C#: http://www.codeproject.com/KB/cs/UsingAOPInCSharp.aspx
NKalore: http://aspectsharpcomp.sourceforge.net/
EOS: http://www.cs.virginia.edu/~eos/
AspectC++: http://www.aspectc.org/
1st conference on Runtime Verification: http://www.rv2010.org/
J-LO: http://www.sable.mcgill.ca/~ebodde/rv//JLO/index.html
SOA: http://msdn.microsoft.com/en-us/library/aa480021.aspx
AOP Introduction: http://sewiki.iai.uni-
bonn.de/_media/teaching/labs/xp/2007b/aop_intro.pdf
Strategies in AOP: http://www.guzzzt.com/files/coding/aspect_strategies.pdf
PostSharp: http://www.sharpcrafters.com/postsharp
Semantics advice: http://www.eclipse.org/aspectj/doc/next/progguide/semantics- advice.html
Runtime Verification Ionut Apetrei:
http://thor.info.uaic.ro/~adiftene/Scoala/2011/TAIP/Courses/TAIP06.pdf
AOP with AspectJ: http://www.tomjanofsky.com/AspectJ.pdf
AspectJ tutorial: http://www.cs.wustl.edu/~mdeters/doc/slides/aspectjtutorial.pdf
AspectJ for Multilevel Security:
http://www.aosd.net/workshops/acp4is/2006/papers/3.pdf
Dynamic analysis of SQL queries:
http://www.info.fundp.ac.be/~staffsem/slides/Cleve.pdf
AOP: http://www.cojan.go.ro/PP/index7.htm, http://www.cojan.go.ro/PP/index8.htm
DeLap, M., et al.: Is Runtime Verification Applicable to Cheat Detection?
http://www.comp.nus.edu.sg/~bleong/hydra/related/delap04runtime.pdf
Sokolsky, O.: Run-time verification, 2006,
http://www.cis.upenn.edu/~alur/CIS673/mac.pdf
Chen, F., Roșu, G. MOP: An Efficient and Generic Runtime Verification Framework.
OOPSLA’07, ACM press, pp 569-588, 2007
Ghoshal, S., Manimaran, S., Rosu, G., Serbanuta, T., Stefanescu, G.: Monitoring IVHM Systems using a Monitor-Oriented Programming Framework, 2008
http://shemesh.larc.nasa.gov/LFM2008/slides/Session2/Rosu.ppt
Model Checking: http://www-2.cs.cmu.edu/~modelcheck/ed-papers/mc.pdf , http://en.wikipedia.org/wiki/Model_checking
Introduction to program monitoring: http://www.runtime-
