Home

Component Reliability Extensions for Fractal component model

1. log log log logs log log log logs log close log close For Logger the situation is more complex log open log log log close Behavior protocols overview This protocol specifies an infinite number of traces as it accepts arbitrary number of calls to log 10g We show the first three shortest traces specified by the protocol log open log open log close log close log open log open log log log log log close log close l1og open log open log log log log log log log log log close log close gt The set of all traces specified by a protocol P is denoted as L P 2 2 Behavior protocol basic operators For behavior protocols the following basic operators are defined sequencing denoted by repetition denoted by alternative denoted by and parallel denoted by and or parallel denoted by We illustrate the meaning of the operators except the last one on the following protocol of the Client component from Figure 1 1 log open log log log log log log log close Client whose behavior is specified by this protocol first calls log open Then it either calls log log twice in parallel orit calls Log Log several times sequentially or it does not call Log log at all as stands for zero or more repetitions At the end it calls 10g close Or parallel is defined as follows if P and Q are p
2. IManagement UsePermanentIpDatabase IIpMacPermanentDb GetIpAddress IManagement UsePermanentIpDatabase IManagement StopUsingPermanentIpDatabase IManagement StopUsingPermanentIpDatabase For testing compliance of the frame and architecture protocols the following input file is created 49 User s manual Figure 6 7 Input file for the behavior protocol checker DhcpServer frame protocol IDhcpCallback IpAddressInvalidated IManagement UsePermanentIpDatabase IIpMacPermanentDb GetIpAddress IManagement UsePermanentIpDatabase IManagement StopUsingPermanentIpDatabase IManagement StopUsingPermanentIpDatabase Ssynchro ops between frame and architecture protocols IManagement UsePermanentIpDatabase IManagement StopUsingPermanentIpDatabase IIpMacPermanentDb GetlIpAddress IDhcpCallback IpAddressInvalidated eop DhcpListener IDhcpListenerCallback RequestNewlIpAddress IDhcpListenerCallback RenewIpAddress IDhcpListenerCallback ReleaselpAddress jo eop Synchro ops IDhcpListenerCallback RequestNewIpAddress IDhcpListenerCallback RenewIpAddress IDhcpListenerCallback ReleaseIpAddress eop IpAddressManager lDhcpListenerCallback RequestNewIpAddress IDhcpListenerCallback RenewIpAddress IDhcpListenerCallback ReleaselpAddress IDhcpCallback IpAddressInvalidated NULL
3. Complementl gt Deterministic2 Deterministic2 label DET fontname Courier Bold Deterministic2 gt Sequence3 Sequence3 label fontname Courier Bold Sequence3 Explicit4 Explicit4 label Exp0 fontname Courier shape invhouse style filled fillcolor grey85 Sequence3 gt Repetition5 Repetition5 label fontname Courier Bold Repetitionb5 gt OrParallel6 OrParallel6 label fontname Courier Bold OrParallel6 gt Explicit7 Explicit7 label Exp1 fontname Courier shape invhouse style filled fillcolor grey85 OrParallel6 Explicit8 Explicit8 label Exp2 fontname Courier shape invhouse style filled fillcolor grey85 Sequence3 Explicit9 Explicit9 label Exp3 fontname Courier shape invhouse style filled fillcolor grey85 Intersection20 gt Adjustment10 Adjustment10 label fontname Courier Bold Adjustment10 gt Explicitl1 Explicitll label Exp4 fontname Courier shape invhouse style filled fillcolor grey85 Adjustment10 gt Explicit12 Explicit12 label Exp5 fontname Courier shape invhouse style filled fillcolor grey85 label Exp0 da open nExpl d insert tr begin da This listing describes the nodes of a parse tree and relations between them each node has an id e g
4. NULL 53 User s manual IDhcpCallback IpAddressInvalidated NULL IDhcpListenerCallback RequestNewIpAddress IDhcpListenerCallback RequestNewIpAddress IDhcpListenerCallback RenewIpAddress IDhcpListenerCallback ReleaseIpAddress IDhcpCallback IpAddressInvalidated NULL IDhcpCallback IpAddressInvalidated IDhcpCallback IpAddressInvalidated NULL yo lManagement UsePermanentIipDatabase IManagement UsePermanentIpDatabaseS IDhcpListenerCallback RequestNewIpAddress IIpMacPermanentDb GetlIpAddress IDhcpListenerCallback RenewIpAddress IDhcpListenerCallback ReleaselpAddress IDhcpCallback IpAddressInvalidated NULL IDhcpCallback IpAddressInvalidated NULL ye IManagement StopUsingPermanentlIpDatabase IManagement StopUsingPermanentIpDatabaseS eop funbound ops none eop After the protocol analysis it can be seen that the event DhcpCallback IpAddressInvalidated emitted from the IpAddressManager component is already accepted by the only instance of its complementary event IDhcpCallback IpAddressInvalidated in the DhcpServer frame protocol So another IDhcp 54 User s manual Callback IpAddressInvalidated event occurring inside of the IDhcpListenerCallback ReleaseIpAddress call cannot be accepted by the DhcpServer component From this it can be deduced that the frame protocol of the Dh
5. we add a behavior protocol to the classic component interface specification For example the behavior protocol of Logger consistent with the plain English specification above reads as follows log open log log log close This protocol consists of tokens denoting method calls log open 10g 10g and log close and operators specifying the ordering of the method calls and Every of these tokens consists of the question mark denoting that the method call is absorbed by Logger and the qualification of the method within the component consisting of the interface name and the method name separated by the dot sign Finally the binary operator stands for sequencing of method calls while the postfix unary operator denotes zero or more repetitions of 10g 1og Therefore this protocol indeed specifies what was written informally above the call of 1og open is absorbed then zero or more calls of log log are absorbed and finally Log close is absorbed Now let us focus on the behavior protocol of Client log open log log Introduction log log log close It differs from Logger in two ways First the method qualifications are preceded with the exclamation mark which stands for emitting a method call Second it specifies that Client calls 10g 10g exactly twice It is correct because Logger is ready to accept an arbitrary number of 10g 10g calls if they occur after Log open and before 1og clos
6. Mehlitz P C Visser W Penix J The JPF Runtime Verification System NASA Ames Research Center available at http javapathfinder sourceforge net PPK Parizek P Plasil F Kofron J Model Checking of Software Components Making Java PathFinder Co operate with Behavior Protocol Checker Tech Report No 2006 2 Dep of SW Engineering Charles University Jan 2006 PPO6 Parizek P Plasil F Specification and Generation of Environment for Model Checking of Software Components Accepted for publication in Proceedings of Formal Foundations of Embedded Software and Component Based Software Architectures FESCA 2006 Vienna Austria ENTCS Mar 2006 73
7. Sequence3 and a label e g The transitions join a parent node with its children e g Sequence3 gt Explicit4 Sequence3 gt Explicit9 In the parse tree diagrams the explicit automata are displayed as gray pentagons and the protocols being represented by such subnodes are displayed at the bottom of the graph In automaton diagrams the initial state is displayed as a rectangle and the accepting states are gray circles with double border Simple examples can be seen at Figure 5 7 and Figure 5 8 Note that the automaton visualization of a more complex protocol may result into a figure having hundreds or thousands of states which will unfortunately not be of much help Here the VRML visualization can be used as an output note that a VRML browser able to handle complex files and hardware fast enough to view the diagrams are needed in this case 35 Implementation Figure 5 7 Parse tree visualization r p a L Expo 3 L eps T x I Lepi J L Expa jJ Exp0 da open Expl d insert tr_begin da imsert lg logEvent tr commit tr abort d delete tr begin da delete lg logEvent tr commit tr abort Exp2 d query da query Exp3 da close Exp4 1da open d msert tr begin da insert lg logEvent tr commut tr_abort d delete tr begin da delete 1g logEvent tr commit tr abort d query da query da close d nsert d query Exp5 da open d insert tr begin
8. m the whole method call from the point of view of the callee and m stands for m m the whole method call from the point of view of the caller In fact in the examples in Chapter 1 only these abbreviations were used to specify the behavior and usage of explicit requests and responses was not necessary We also define two more complex abbreviations if P is an arbitrary protocol m P means that the call request of m is absorbed and while m is processed the component behaves as specified by P af terwards the call response of mis emitted In a similar way m P means that P specifies the behavior of the caller between issuing the call of m and receiving the response of m The abbreviations not only serve as syntactic sugar allowing to write readable behavior protocols but they also explicitly denote pairing of events requests and corresponding responses In certain situations such information is essential for the behavior protocol checker This is why for certain types of inter faces only an abbreviation can be used to specify the method call and the use of explicit event spe cification is forbidden see Section 4 5 1 A computation of a component application is formally described by a trace a finite sequence of event tokens Every protocol specifies a set of traces Recall the protocol of C1ient from Figure 1 1 log open log log log log log close It specifies a single trace llog open log open
9. protocol valuez log open log log log close lt component gt lt binding client client log server logger log gt lt binding client this run server client run gt lt definition gt Once having specified the behavior protocols of the components the compliance of the components can be checked easily by a special FractalADL launcher java org objectweb fractal behprotocols staticchecker Launcher check logger LoggerDemo Checking for compliance OK The response indicates that the two components in our example have compliant behavior protocols 6 1 2 Launcher Checking of protocol compliance is realized by a special Fractal ADL application launcher java org objectweb fractal behprotocols staticchecker Launcher check definition itf The argument definition is the ADL file containing the definition of the component to be instantiated and started The argument iff is the name of the top level component s Runnable interface if it has such If not given an interface named run is assumed By default the component is run without checking of protocol compliance The checking can be selected with the check switch In this case the component application is only instantiated without being started and checked The results are printed out to the standard output The meaning of the error reports is explained in Section 6 3 1 6 1 3 Configuring Julia The protocol checker uses the runtime representation of
10. 22 4 4 2 Controllers RuntimeCheck and LifeCycle sss seen sean sean eeee 24 4 4 3 Handling protocol violations esses He emen menrennne 24 4 44 Technical notes oreet rper E tue erbe e REPRE 25 4 5 Extensions to protocols tte tete tet pier eoe mi E Ud pe e E ee EHE evenit a EYE d 25 4 5 1 Multiple bindings rettet tert te pice ptores presb E 25 4 5 2 ATOMIC detlons cuoio RU ERE pe bI e EVI I a 27 4 5 2 1 OVERVIEW ious shee uec trece re PERPE SERERE ERR dh sects MEE ERR 27 AD 2D SyDtax o dihaugelaceere e DIDI ERU PRISES 27 4 5 2 3 Sem ntics cote Ek E ERR RS shoes Ee RSEN ERY EO Ese E rE E Pec ce Y veh 27 4 5 2 4 Notes c iie ree erts nto E ie ort to Sedet egre i doe Suse eod gee re tr geste peccet epus 27 4 6 Checker enhancements os inimi rer eT EE RR UE Per Pes Rer e ER TRESE PEETERS eS 28 4 6 1 Static checking 2 cete UI E Wonca bys e ee E ER 28 4 6 1 1 Incomplete bindings itt te tete er terere te reso SEDI 28 4 6 1 2 Collection interf ces osito voce ede webu odes ue se Pee ep Regi se 28 4 6 1 3 Multiple bindings ciere ERI ERR E ESTEVA ERR enn 28 4 6 1 4 Atomic ACTIONS iioi ce meret ett prre e EE EEE E EEEE aeS 28 4 6 1 5 Substantial performance improvements sssssssesse eme 28 4 6 2 Run time checking eei e termed te tpe ce mr ete ene reor edge i ye cueveee 29 4 7 Cooperation of Java PathFinder with protocol checker ss seca
11. Command line Reference The checker can be used as a part of the SOFA and Fractal environments or as a standalone tool This section focuses on the latter case The syntax of the command line when using the checker as a stan dalone tool is the following java jar checker jar actionl a testltestconsentlvisualizedot verbosel v 2 0l1122 nomultinodesl m noexplicitl e noforwardcutl f nobadactivityl b nonoactivityl n ifiniteactivityl i nolnotracelyes totalmeml t 2 size cachesizel s lt size gt lt filel f lt inputfile gt lt protocoll gt provisions 1 2 lt protocol2 gt provisions 2 3 lt protocol3 gt unbound operations The parameters have the following meaning actionl a test the checker will perform the test for composition errors and consensual compliance of an inverted frame protocol lt protocol1 gt and the composition of the other protocols the protocols are composed from back to front i e protocol n and protocol n 1 are composed first In the case the protocols are not consensually compliant or a composition error is detected a counterexample i e the trace that cannot performed by both of the two components behaving according to the first and the second protocol respectively is provided and an html file denoting the actual position within the pro tocols is created action a testconsent the checker will perform the composition t
12. IDhcpCallback IpAddressInvalidated NULL 50 User s manual IDhcpListenerCallback RequestNewIpAddress IDhcpListenerCallback RenewIpAddress IDhcpListenerCallback ReleaselpAddress IDhcpCallback IpAddressInvalidated NULL IDhcpCallback IpAddressInvalidated NULL yx IManagement UsePermanentIpDatabase IManagement UsePermanentIpDatabaseS IDhcpListenerCallback RequestNewIpAddress IIpMacPermanentDb GetlIpAddress IDhcpListenerCallback RenewIpAddress IDhcpListenerCallback ReleaselpAddress IDhcpCallback IpAddressInvalidated NULL IDhcpCallback IpAddressInvalidated NULL IManagement StopUsingPermanentIpDatabase IManagement StopUsingPermanentIpDatabaseS eop unbound ops none eop Checker can be run using following command java jar checker jar action test f compliance bp The checker would report a bad activity error in this case 51 User s manual Composition error detected bad activity IDhcpCallback IpAddressInvalidated 0 1IDhcpListenerCallback RequestNewIpAddress 5 IDhcpListenerCallback RequestNewIpAddress 6 4IManagement UsePermanentIpDatabase 7 1 1 IDhcpCallback IpAddressInvalidated me S S S S S14 4IDhcpListenerCallback ReleaseIpAddress S15 To find out the reason of the bad activity we need to analyze the input protocols and the error trace ou
13. IFlyTicketAuth CreateToken ava IFlyTicketAuth CreateToken ava IFlyTicketDb GetFlyTicketsByFrequentFlyerId ava ICsaFlyTicketDb GetFlyTicketsByFrequentFlyerId ava ICsaFlyTicketDb GetFlyTicketsByFrequentFlyerId Cs ocio Us Xe C ds CI CI Uds sll CHR ode 67 User s manual java rtcheck AfDbConnection protocol satisfied java rtcheck CsaDbConnection protocol satisfied java rtcheck FrequentFlyerDatabase protocol satisfied java rtcheck Timer protocol satisfied java rtcheck DhcpListener protocol satisfied java rtcheck TransientIpDb protocol satisfied java rtcheck IpAddressManager protocol satisfied java rtcheck ValidityChecker protocol satisfied java rtcheck Timer protocol satisfied java rtcheck ValidityChecker protocol satisfied java rtcheck Timer protocol satisfied java rtcheck ValidityChecker protocol satisfied java rtcheck Timer protocol satisfied java rtcheck FlyTicketDatabase protocol satisfied java rtcheck DhcpServer protocol satisfied java rtcheck org objectweb dsrg behprotocols demo Token protocol satisfied java rtcheck org objectweb dsrg behprotocols demo Token protocol satisfied java rtcheck org objectweb dsrg behprotocols demo Token protocol satisfied BUILD SUCCESSFUL Total time 17 seconds In this demo we have intentionally made the FlyTicketClassifier component non compli
14. Protocol Checker l log log PR 3 notify log log Lor 4 Hog Jog JPF Protocol Listener oa Checker _ 10 ok 9 Plog log 6 return 7 return insn While implementing the mapping between the JPF state space and the checkers state space we had to make two modifications to the JPF source code First we had to modify the code responsible for partial order reduction so that a transition between states is terminated when an invoke or return in struction corresponding to a method of a frame interface of a target component is executed Second we had to enhance the JPF search engine which drives the traversal of the state space so that JPF asks the checker for a permission to backtrack we call this coordination of backtracking For motivation of the changes to JPF please see PPK 30 Chapter 5 Implementation 5 1 Behavior protocol checker static version 5 1 1 Implementation overview The behavior protocol checker was implemented in Java using sdk 1 4 2_03 version 1 5 is not supported since Java PathFinder doesn t support the 1 5 version bytecode and a preliminary version has been a part of the SOFA technology see http sofa objectweb org The checker has been substantially en hanced now the checking process is much more efficient in both memory and time requirements A rough structure of the behavior protocol checker is depicted on Figure 5 1 The protocols to be
15. Run time checker sesessessesen HH Here 59 6 4 1 Getting started oos t oe een ee eoo teneo puto deep es amie ee dot 59 6 4 2 Julia Conf gs Uration o Re ee er te cu te rte e eai eie e vede 59 6 4 3 Running a runtime checked application sssssessee eme 62 6 4 4 Case Study Applying runtime checker on the Airport internet lounge demo 65 6 5 Code analysis of primitive components esseessssesesseeeeee eee Hee Hene eee hene nhe 68 6 5 Getting started o CS E o ede ee REA dc ed td 68 6 522 Julia Configuration esee tiet hao Teo coepere thee Gee d setate Des Cep dna ou mE ULP eed ce ue Oe Pes Mone dane tes 68 6 5 3 Running the check of primitive components sssssessessee eee em emen 69 6 5 4 Case Study Applying code analysis on the Airport internet lounge demo 71 References c e Ree ede ode D eee de T des D M oi RI vera et pe EE ue oe pe wees 73 Chapter 1 Introduction 1 1 Fractal Fractal is a component model developed initially by France Telecom and INRIA and later as an open source project in the ObjectWeb consortium The component model is defined by the Fractal Component Model specification BCS The specification defines a hierarchical component model where a com ponent is specified in terms of its server and client provided and required interfaces and configurable attributes The model supports advanced features such
16. as component sharing mandatory optional in terfaces collection interfaces The Fractal API is defined for three languages Java C and CORBA IDL The reference implementation of Fractal Julia is developed in Java and supports Java Fractal components The Fractal specification allows to use an Architecture Description Language ADL however it does not directly specify one In the Fractal ADL project an XML based ADL for the Fractal component model is defined to specify the initial architecture of an application The features of this ADL language include inheritance among component specifications and also a mechanism to specify values of components attributes 1 1 1 Basic assumptions The Fractal component model specification is very flexible and structured in several conformance levels consequently many concrete component systems comply with it To make the integration of behavior protocols into Fractal possible we take the following additional assumptions 1 In Fractal every component has internal and external interfaces We suppose that for every external interface there exists an internal interface of the same type and vice versa In addition an event on an external interface immediately causes the complementary event on the corresponding internal inter face and these two events happen atomically In a similar way an event on an internal interface imme diately causes the complementary event on the corresponding external
17. called at ServerImpl print ServerlImpl java 35 at org objectweb fractal julia generated C3b8aff70 0 N print INTERCEPTOR Service at org objectweb fractal julia generated C41c1ff86 0 print INTERCEPTOR Service at org objectweb fractal julia generated C2deafae5 0 print INTERCEPTOR Service at org objectweb fractal julia generated Ca0b05alf 0 print INTERFACE Service at org objectweb fractal julia generated C9ec05a0f 0 print INTERCEPTOR Service at Clientimpl run ClientImpl java 35 at org objectweb fractal julia generated C600cae0c 0 run INTERCEPTOR Runnable at org objectweb fractal julia generated C78281da2 0 run INTERCEPTOR Runnable at org objectweb fractal julia generated C78281da2 0 run INTERCEPTOR Runnable at org objectweb fractal julia generated C6a0cd3b 0 run INTERFACE Runnable at org objectweb fractal behprotocols adl Launcher main Launcher java 105 Server begin printing hello world Server print done rtcheck client protocol satisfied rtcheck server protocol satisfied rtcheck WrappedHelloWorld protocol satisfied rtcheck clientWrapper protocol satisfied rtcheck serverWrapper protocol satisfied A variation of this example featuring incorrect protocols is available in the file WrappedHello WorldIncorrect fractal The runtime check framework can in principle detect two kinds of errors bad activity event occurring when not permitted by the
18. da insert lg logEvent tr commit tr abort tr pause tr resume d query da query da close Figure 5 8 Automaton visualization 5 1 6 Further information For detailed information about the classes details see the checker javadoc documentation javadoc index html 5 2 Implementation of the runtime checker 5 2 1 Overview The implementation of the runtime checker exploits a lot of functionality of the static checker imple mentation The core part of the static checker i e the on the fly generation of the transition graph can be reused without any changes As the state space is not exhaustively traversed during the runtime 36 Implementation check but the traversal is driven by the information about method calls provided by the component interceptors only one transition at a point representing the event being performed is taken 5 2 2 Atomic actions Atomic actions need to be handled in a special way during the runtime checking As only one event may be executed in each step and a protocol containing an atomic action thus can t be satisfied at runtime checking each atomic action is replaced with a protocol consisting of atomic action events combined using the and parallel operator expressing the necessity that each of the atomic action events has to be executed but the order doesn t matter The transformation is done during the protocol parsing process so it is invisible to the other parts of the
19. efficient state representation for storing information about visited states and for state comparison is needed In the current version of the behavior protocol checker a state is represented as a bit field Management of such state identifiers is easy and very fast however the drawback of this representation is that because of possible non determinism it is not possible to determine the exact state identifier size in advance sizes for different states may even differ Thus there may be some unnecessary memory reallocation needed during checker computation but this is probably inherent for any memory reasonable representation Since the generation of possible transitions from the current state is the far most time consuming op eration of the compliance checking process this operation is optimized for the best performance using state pregeneration and by computing all the information not depending on the current states in advance 28 New features developed within this project This optimization has further improved the performance of the checker without significant increase in memory requirements For more information about the optimization included in the checker please refer to Section 5 1 3 4 6 2 Run time checking The checker is able to check if the real time behavior of a component conforms to its declared behavior specified by its frame protocol The runtime checker does not perform an exhaustive traversal through the st
20. goes through a given component nesting hierarchy and on each level of nesting it checks the compliance of a component s frame protocol with the architecture protocol constructed from the frame protocols of the component s direct sub components The parameter passed to the checker is the root component of the nesting hierarchy that is to be verified Thus in the example bellow we pass to the checker the application s top level component System out print Checking for compliance NestedCheckingResult res ProtocolChecker check rootComp if res getErrorType NestedCheckingResult ERR OK System out println Error System out println res toString else System out println OK The meaning of the output is described in detail in 5 3 6 2 3 Configuring Julia Again as in the case of instantiating components using Fractal ADL it is necessary to customize the Fractal implementation used in order to attach a protocol controller to newly created components The way a protocol controller is attached to a component is specific to a particular Fractal implementation In the case of Julia this is achieved by modifying the Julia configuration e g julia cfg as described in 5 1 3 6 3 Protocol checker user manual for the standalone version 6 3 1 Getting Started 6 3 1 1 A sample component design The following picture shows an example of a composite component DhcpServer The DhcpServer component contains t
21. had to define a mapping from the JPF state space into the state space of the checker to make such cooperation possible For more information on the mapping please refer to PPK 4 7 1 Checker for code analysis We have modified the behavior protocol checker for static testing by adding several methods to make the cooperation with JPF possible In particular the checker has been enriched by a method for noti fication of actions performed method called and finished in the JPF and uses this for coordination of the state space traversal Each time JPF moves along a transition corresponding to a method call or return from a method call it notifies the checker of this event Checker moves along the corresponding transition in its own state space Should not such a transition exist within the checker s state space an error is reported to the user and the implementation is considered not to be bound by the protocol To treat all the combination of implementations and protocols correctly as well as to be able to handle cycles it is necessary to coordinate the traversal in the following way Each time JPF would backtrack within the state space because of being in an already visited state it asks the checker for permission Only in situations when both JPF and the checker would backtrack at this point when executed on their own i e if being in an already visited state backtracking is allowed Hence the bounding relation can be checked correctly 4
22. in the original program Consequently a model checker may then find errors that are not present in the program i e false negatives Fortunately there exist model checkers that work directly with the implementation of a target system Java Pathfinder is an example of such a model checker Properties to be checked are usually expressed via temporal logic CTL LTL or in the form of asser tions Some model checkers are also able to check for a fixed set of special properties deadlocks un caught exceptions etc The biggest problem of model checking with respect to practical use of this technique is the size of the state space typical for software systems the problem of state explosion However decomposition of a software system into components helps to mitigate the problem A component usually generates smaller state space than the entire system and therefore can be checked with fewer requirements on space and time In our case we use model checking to check whether a primitive component is bounded by its frame protocol or not And since most implementation of the Fractal Component Model are Java based in cluding the reference implementation Julia we decided to use the Java PathFinder model checker JPF JPF 3 1 Environment Although model checking of individual software components helps to mitigate the problem of state explosion a component cannot be checked in isolation because it does not form a complete program with
23. interface and the two events happen atomically 2 Interfaces in Fractal are connected by bindings We suppose that an event occurring on an interface I causes immediately the complementary event on the interface I is bound to and the two events happen atomically assuming I is bound to exactly one interface If I is bound to more interfaces the events on those interfaces do not have to happen atomically 1 2 Behavior protocols The purpose of behavior protocols is to specify the behavior of software components so that interesting properties of their behavior can be verified The problem of behavior verification is undecidable in general There are two ways to face it 1 To use behavior description languages which describe behavior of the software precisely and to put up with the fact that the tools will never stop for some inputs behavior descriptions 2 To use behavior description languages which are not expressive enough to describe behavior of software precisely but the verification of the specifications is decidable We have chosen the second approach Therefore a behavior protocol should be seen rather as an approximation of a component s behavior The most important benefit of this approach is the existence of a fully automatic behavior verification procedure implemented in our behavior protocol checker The main difference between full description of a component behavior and a corresponding behavior protocol is that the
24. object this approach would not address interceptors associated with collection interfaces For a collection interface the interface object is created by cloning a template interface object only at the time the particular interface name is used for the first time A new instance of the interceptor object is created cloned while cloning the interface object To properly handle this situation the responsibility for initializing the interceptor object must be assigned to the interface object In the newly introduced BasicIdentityAwareComponent Interface class we have overridden the setFcItfName method of the BasicComponent Interface class to call the setter method of the interceptor object if the interface has an interceptor and the interceptor implements the Iden tityAwareInterceptor interface Hence to properly handle collection interfaces it is necessary to use a customized interface object using BasicIdentityAwareComponentInterface instead of BasicComponent Interface as the base class We show the relevant fragment of the config uration file in Figure 4 6 Figure 4 6 Fragments of the Julia configuration file related to interface objects interface class generator org objectweb fractal julia asm InterfaceClassGenerator org objectweb fractal behprotocols julia BasicIdentityAwareComponentInterface We would also like to document one technical aspect related to future extensions of Julia In its initial design Julia was supposed
25. run s print gt lt component gt component name serverWrapper interface name s role server signature Service component name server interface name s role server signature Service gt content class ServerImpl attributes signature ServiceAttributes gt attribute name header value gt attribute name count value 1 lt attributes gt lt controller desc primitive gt lt protocol value s print gt lt binding client this s server server s gt lt protocol value s print gt lt component gt lt binding client this r server clientWrapper r gt lt binding client clientWrapper s server serverWrapper s gt protocol value r run r run gt lt definition gt By running the HelloWorld example with the command ant execute we obtain the following output CLIENT created SERVER created starting checker for component client with protocol r run s print starting checker for component server with protocol s print starting checker for component WrappedHelloWorld with protocol r run r run 63 User s manual starting checker for component clientWrapper with protocol r run s print starting checker for component serverWrapper with protocol s print Server print method
26. the definition of frame and architecture we also distinguish between frame protocols and architecture protocols Frame protocol of a component C describes requests and responses on the frame of C The frame protocol is specified by the developer The architecture protocol of C is auto matically constructed from the frame protocols of C s direct subcomponents by the behavior protocol checker It describes what is happening inside C In the architecture protocol of a component C two types of events appear events on the frame of C and events resulting from the communication of C s direct subcomponents internal events The first type of events is denoted in the same way as in frame protocols The prefix is used in both event tokens and abbreviations to denote internal events Section 2 1 For example the architecture protocol of the C1ient component from Figure 2 1 reads as follows lt A logl log gt open lt A nt1 B nt2 gt notify lt B log2 log gt log lt A logl log gt log lt A logl log gt close Formally the composition of subcomponent frame protocols resulting in the architecture protocol is defined by the consent operator APO5 This operator is never used by the designer specifying the frame protocols it is only a formalization of the behavior composition which is done automatically by the behavior protocol checker Behavior protocols overview 2 4 Static checking 2 4 1 Protocol complia
27. the get ImplementedInterfaces method specified in the ClassGenerator interface We have introduced the get ImplementedInterfaces method also into the CodeGen erator interface and extended InterceptorClassGenerator getImplementedInter faces to merge requirements from all its subordinate CodeGenerator objects To handle this modification of the CodeGenerator interfaces we have provided a default imple mentation of this newly introduced method into all the Julia classes implementing this interfaces SimpleCodeGenerator and MetaCodeGenerator These extensions have been committed to the Julia CVS repository and have been included in the recent release of the Fractal project 2 3 1 The subsequent task was to use these extensions to introduce identity aware interceptors Here we consider the identity of an interface to consist of its name isClient value contingency mandat ory optional cardinality singleton collection and signature type While the runtime checking framework is particularly interested only in the name and isClient value we have decided to intro duce more general extensions realized in the IdentityAwareInterceptor interface see Fig ure 4 5 Here an additional way to express the identity of an interface is via a reference to the interface object which allows to obtain the interface type via the get FcItfType method to access the addi tional attributes 22 New features developed within this project Figu
28. to support reconfiguration of a single component instance in particular optimizing deoptimizing the component This vision included also dynamically introducing removing interceptor objects this would likely be done via the setFcItfImpl method of the Component Int erface interface As such a reconfiguration is not used in Julia we do not provide any special means to handle it i e to update the interface identity stored in the identity aware interceptors possibly in volved Should a need arise to do so it would be possible to modify Julia to support such a reconfig uration Changes would have to be introduced into the set Fc It f Imp1 method featured by interface 23 New features developed within this project objects as the implementation of this method is generated by the InterfaceClassGenerator it would be necessary to modify the way it is generated The method could either update the identity directly or it might call a method inherited from the interface object base class introducing the setItflImpl method into the base class would also make future extensions related to dynamic re configuration much easier 4 4 2 Controllers RuntimeCheck and LifeCycle The key responsibility of the RuntimeCheckController is to manage the checker backend to collect events from the interceptors and to pass these events to the checker backend Furthermore the RuntimeCheckController may also collect information on the component execution c
29. 7 2 Extensions to the Java PathFinder The mapping between JPF and the checker needed for code analysis is implemented via a JPF listener i e via a plugin for JPF During traversal of the JPF state space the listener traces execution of all invoke and return byte code instructions that correspond to methods of the provided and required in terfaces of a target component and notifies the checker about such instructions This way the listener instructs the checker what transition to take in its state space The notification is done also during backtracking in order to instruct the checker to also backtrack 29 New features developed within this project Additionally the JPF listener also notifies the checker when it reaches an end state In that case if the protocol checker is not in an end state of its state space an error is reported This can happen for ex ample when JPF comes to the end of the main method in its state space but the checker still expects some more events to occur Communication between JPF and the checker during the checking of the Client component see Section 2 6 is shown on Figure 4 9 The left part shows the JPF state space and the right part shows the state space of the checker numbers determine the order of related activities in JPF and the checker Figure 4 9 Communication between JPF and Checker during traversal of state spaces in the onward direction State space of State space of Java PathFinder
30. Client llog1 open llog1 log llog1 close llog2 log llog open llog log log log llog close On Figure 1 2 there is an example of an implementation of the Client component Client consists of two subcomponents A and B whose behavior protocols are also in Figure 1 2 To check the compliance the first task is to figure out the behavior of A and B being run simultaneously In this case it is simple as A and B do not communicate with each other therefore the behavior of Client s internals is lt A logl log gt open Introduction lt A logl log gt log A logl log close B 10g2 log log There are several new constructs in this protocol First it does not specify behavior of a component but the behavior of a group of components Therefore to fully qualify a method it is not more suitable to use the local name of the interface Instead name of the binding is employed For example lt A logl log gt identifies binding between the 1091 interface of the A subcomponent and the log interface of the supercomponent from the context Client is known to be the supercomponent here this is why its name is not used to prefix the 10g interface name Second the binary operator stands for parallel execution of two subprotocols This is what is needed to be expressed the subcomponents A and B run independently on each other The behavior of internals of the Client component is not c
31. Component Reliability Extensions for Fractal component model Architecture Design manual and User manual Final deliverable T0 18 Jiri Adamek Tomas Bures Pavel Jezek Jan Kofron Viadimir Mencl Pavel Parizek Frantisek Plasil Component Reliability Extensions for Fractal component model Architecture Design manual and User manual Final deliverable T0 18 by Jiri Adamek Tomas Bures Pavel Jezek Jan Kofron Vladimir Mencl Pavel Parizek and Frantisek Plasil Table of Contents T Introduction o ict ses boe e eo ore ete pe pat sa DER I see ELE tel sa oat se De pte ae re taxe EO A E catus 1 1 1 Fractal iie LERRA CENSET n Lp UE 1 LTA Basic assumptions deo aerea yess vd Ee ehe vom ds ES ERR ER RR UPRR EE ES EEEE E MER CERRAR ERE RES TER 1 1 2 Behavior protocols oer Wis eaves costa wecuotelacccis inoue bead Mee tee ETUR UE MEE PER Eee E Te ERU 1 1 22 Behavior protocol Dasi Seia ee rete rte OR CER REX ERSTE ERE UE EET 2 1 2 2 Static checking iecore been n Poe side tete tee he sse Petty ve eerte p ee eie eee 3 1 2 3 Verifying behavior of primitive components ssssssssss ee 4 12 331 Run time checking crisare ete eie rere RUE rele r ev Ince era tees 4 1 2 3 2 Code analy SiS 4 ectetuer arte i pre trt Recap Ee 4 2 Behavior protocols overview esses mee mee ee he nhe hee rentes meet ee hee he nee eee nennen 6 2 1 By nts and traces nier Rec ede D CREE REPE RPM 6 2 2 Behavior protoco
32. Finder essssssse emere 37 6 Users manual 315 sta WI eats dei es o an eS 39 6 1 Fractal ADL protocol checking eiie tase oet e ettet re teer Set agar DRE Roe Po Ut de de eite 39 6 1 Gettmng started ooo e mie p edP iet pte to aeg ted 39 6 12 Eaunchet ee rere e pines oot de ses tende ea Doreen ose petuo de IN EEES 40 6 13 Confhig ring Julia idR esee Po ee SOC eee qe ed olv eu P DRE 40 6 2 Building application directly from code sssssssessessee emm HH He 41 6 2 1 Associating a protocol with a component instance sese 41 6 2 2 Checking instantiated components sss emen mene 42 6 2 3 Conhig ring Julia 3 rU Ds E e S e Ve Ur ea S ORE e E LPR SUI 42 6 3 Protocol checker user manual for the standalone version eee 42 6 3 15 Getting Started 5 ee eoe ed io eek ld Peters d edt pep Cr eee EE eae 42 6 3 1 1 A sample component design ssssessessee Here 42 6 312 Writing protocols rion o ene ve dene ste eee Pr ase ere Qo 43 6 3 1 3 Checking for compliance 3 e ttd ere ette ee dawn trt adopte dete 47 6 3 1 4 Checking for incomplete bindings ssseee HH 55 6 3 2 Command Ime Referen e eee coser doner dont i erbe e tins e eee dee eo to ek e tene ee Mie DERE e een Du 56 6 33 Vis Wali zation casei e RE RM Ue RI REPE Ro RR EE eh a 57 6 3 4 Example of protocol input file sss eene ener 58 6 4 Fractal extensions
33. allback IpAddressInvalidated NULL ys IManagement UsePermanentIpDatabase IManagement UsePermanentIpDatabaseS 46 User s manual IDhcpListenerCallback RequestNewIpAddress ITIpMacPermanentDb GetIpAddress IDhcpListenerCallback RenewIpAddress IDhcpListenerCallback ReleaselpAddress IDhcpCallback IpAddressInvalidated NULL IDhcpCallback IpAddressInvalidated NULL yx IManagement StopUsingPermanentIpDatabase IManagement StopUsingPermanentIpDatabaseS eop unbound ops none eop Lines beginning with the sign are just comments The only exception is eop which means End Of a Protocol This token serves as a delimiter and allows an input file to use advanced protocol formating to improve readability The file contains three types of sections Each section is separated by the eop delimiters or by the start or the end of a file The first section type contains frame protocols The first protocol is a frame protocol of the architecture while the other protocols describe the subcomponents behavior Between each two protocol sections there is a synchro operation section This section type contains synchro operations that represent all methods of the interfaces bound between the two components The third section type is the last section This section enumerates all methods of unbound interfaces i e operations that should not be performed if i
34. ame time note that this is stronger than just a simple parallel operator However the runtime checker is not multithreaded and all method callbacks from the Julia interceptors are processed in a sequential order This means that is makes no sense to use the atomic actions in runtime protocols Our solution was to replace all atomic actions with other standard behavior protocol constructs The Fractal implementation demo is in fact a set of independent components that are only connected to communicate with each other However as the components are designed to serve to the users of the system none of them is able to work autonomously In order to function the components must receive requests from the outer world their environment The three components responsible for such communication are the DhcpServer component more precisely one of its subcomponents the Dh cpListener the Arbitrator and the AccountDatabase To simulate the environment of these components we created the Simulator component It implements a simple hard wired test of all the client accessible methods of the demo components i e it emulates requests accepted from 3 virtual clients passed to the Arbitrator component via a virtual web server and also calls several methods on the DhcpListener component simulating the DHCP protocol packets coming from clients Here is the main part of the Simulator run method iArbitratorLifetimeController Start byte macl ne
35. ames names of unbound interfaces remain unmodified In the second step the protocols are composed using the consent operator The purpose of the first step of the algorithm is to ensure that the emission and absorption of any event specified in different frame protocols is denoted by tokens which differ only in the prefix or If this was not the case the consent operator would not work correctly To guarantee proper functionality of the consent operator also in the presence of multiple bindings the first step of the algorithm has to be modified The idea behind the modification is the following If a provided interface has multiple bindings and the protocol of its component denotes acceptance of 25 New features developed within this project a method call on the interface the call will be absorbed from just one of those bindings On the other hand if a required interface has multiple bindings and the protocol of its component denotes that a method call can be emitted on the interface the method will be called on all of the bindings multicast As taking an assumption on the order of the calls would be too restrictive the calls on those bindings are considered to happen in parallel Every particular ordering of the calls is compliant with this as sumption Formally the protocols are transformed as follows a Names of unbound interfaces remain unmodified b Name of an interface which has exactly one binding is replaced
36. ance of the two inner components IpAddressManager and DhcpServer together The behavior protocols of these two components follow 43 User s manual Figure 6 3 IpAddressManager Behavior Protocol IDhcpListenerCallback RequestNewIpAddress IDhcpListenerCallback RenewIpAddress IDhcpListenerCallback ReleaseIpAddress IDhcpCallback IpAddressInvalidated NULL IDhcpCallback IpAddressInvalidated NULL IDhcpListenerCallback RequestNewIpAddress IDhcpListenerCallback RenewIpAddress IDhcpListenerCallback ReleaselpAddress IDhcpCallback IpAddressInvalidated NULL IDhcpCallback IpAddressInvalidated NULL k IManagement UsePermanentIpDatabase IManagement UsePermanentIpDatabaseS IDhcpListenerCallback RequestNewIpAddress IIpMacPermanentDb GetlIpAddress IDhcpListenerCallback RenewlpAddress IDhcpListenerCallback ReleaselpAddress IDhcpCallback IpAddressInvalidated NULL IDhcpCallback IpAddressInvalidated NULL 44 User s manual IManagement StopUsingPermanentlIpDatabase IManagement StopUsingPermanentIpDatabase Figure 6 4 DhcpListener Behavior Protocol IDhcpListenerCallback RequestNewIpAddress IDhcpListenerCallback RenewIpAddress IDhcpListenerCallback ReleaselpAddress To check the compliance of these two protocols we need to prepare an input file for the static behavior checker The file will con
37. ant with its protocol This is reported as the ProtocolViolationException along with the trace that lead to the protocol violation The other protocols were satisfied as reported in the output 6 5 Code analysis of primitive components 6 5 1 Getting started Code analysis of primitive Fractal components is performed by the Java PathFinder model checker JPF in cooperation with the protocol checker for code analysis The tool accepts a program composed from a target primitive component and its environment as input and traverses both the state space determined by the program and the state space determined by the protocol The easiest way to apply code analysis to an application is to start the application augmented with behavior protocol specifications Section 6 1 1 and also with necessary information for the environment generator Section 6 5 3 6 5 2 Julia configuration The environment generator must at runtime get for a component being checked the information stored in the ADL definition of the component This includes the data provided by the protocol and environment controllers i e the frame protocol of the component the name of the class with value sets etc Therefore an environment controller has to be attached to each component in a similar way as it is done for protocol controller Specifically it is necessary to extend the Julia configuration 1 e the ju lia cfg file in the following way Protocol Controller in
38. apturing its execution trace and the list of method calls currently in progress this information may be used by a monitoring toolset The interface of the Runt imeCheckCont roller is shown in Figure 4 7 The controller functionality is implemented in the BasicRuntimeCheckControllerMixin class Please note that the event tokens are internally stored as strings the notation is the same as the one used by the checker backend i e the event token string starts either with an exclamation mark for an event emitted or with a question mark for an event absorbed followed by the name of the interface concatenated with a dot with the name of the method followed by a either the character to denote a method request or by to denote a method response For a pair of events forming a single procedure call the initial character of the request or is the opposite to the initial character of the response Both the operations get FcCurrentMethods and getFcMeth odHistory return an array of strings following this format The runtime checking subsystem is inherently tied with the lifecycle of the component being monitored When the component starts monitoring has to start with the protocol configured for the component When the component stops it is necessary to verify that the protocol permits to stop at the given point in the components execution history i e whether the corresponding automaton managed by the check
39. ate space defined by the protocol as in the case of static checking but the state space traversal is driven by the information about method calls provided by the component interface interceptors Should an event violating the frame protocol occur i e the event is not among events allowed at this particular point with respect to the history of events there are two options 1 the application is stopped or 2 an error message is printed to the output and the application continues but no further checking is performed as there is no method known for recovering from such a state At the end of the application run the checker provides information whether the component has successfullly satisfied its frame protocol i e whether an accepting state has been reached 4 7 Cooperation of Java PathFinder with protocol checker As already said in Chapter 3 we use JPF for checking primitive Fractal components implemented in Java against behavior protocols However it is not directly possible to use JPF for checking whether a primitive component is bounded by a protocol because JPF is by default able to check only prop erties like deadlocks and assertions In order to solve this we decided to use JPF in combination with the protocol checker for code analysis In other words we decided to let JPF and the checker cooperate on code analysis while traversing their own state spaces Since JPF and the checker work at different levels of abstraction we
40. bound requires error occurs when a component tries to call a method on its required interface which is unbound 10 Behavior protocols overview Figure 2 3 Example of incomplete bindings interface Choose void a interface Notification void b void notify d LAS ch a ch b nt notify S y An example of a component application with one unbound required interface the nt interface of the A component is shown on Figure 2 3 On the ch interface of A the a or the b method can be called If b is called A reacts by calling nt notify As the B component calls only ch a the A nt no tify method is never called and the fact that A nt is unbound does not cause any problem On the other hand if the behavior protocol of B was ch b it would result in an unbound requires error More information on incomplete bindings can be found in AP04 2 5 Run time checking The run time checker monitors the events on the external interfaces of a component the trace and checks whether this trace is one of those specified by the frame protocol of the component If not it is considered to be an error The main reason for using the run time checker is verification of the composite components with dy namic architectures which cannot be verified statically Also run time checking is an alternative to static checking in the situations when the architecture of a composite component is
41. byte code which works as a specialized Java Virtual Machine JPF VM Unlike standard Java VM the JPF VM executes the program in all possible ways with respect to threads instructions interleaving and values of input data Using this approach the state space of the target program is generated on the fly as JPF executes the program JPF integrates several methods for decreasing the state space size Like majority of other model checkers it supports partial order reduction POR CGP It is based on the idea that some instructions or sequences of instructions are commutative when executed concurrently i e they result in the same state regardless of the order of their execution Actually JPF implements POR in a slightly indirect way it executes instructions of the current thread one after another till the current instruction is scheduling relevant e g it accesses a shared variable starts stops a thread blocks a thread etc or a value selection via the methods of the Verify class takes place Important feature of JPF is its extensibility via the publisher listener design pattern which allows to observe the course of the state space traversal and to check for specific properties in each state This can be done at two abstraction levels 1 virtual machine listeners provide low level VM information for checking of complex properties and ii state listeners used for basic checks requiring information about visited states This is especial
42. c Sabo God As the state space of a more complicated protocol may be very large the memory available for the checking may become insufficient state explosion problem To solve this problem i e to be able to check compliance of such protocols we use on the fly automata that are generated during the compu tation as needed This greatly enhances the usability of the checker The drawback of this method is the lower speed of the checking compared to the state space pregeneration approach To improve the performance we use optimizations such as explicit automata forward cutting multinodes for more information see PTA 5 1 2 Basic structure and interaction The checker can be used as a standalone tool and is also integrated into the Fractal environment In teraction with the Fractal application is realized via the FractalStaticChecker class The first thing to be done here after protocol transformation to handle multiple bindings is parsing the input protocols and building parse trees While constructing the parse tree the multinodes optimization is applied if there are more than two operands of the same binary operator sequence alternative and parallel where a subtree Figure 5 3 should be build the nodes are instead collapsed into a single multinode Figure 5 4 Figure 5 3 Original parse tree P Figure 5 4 Multinode optimization The resulting parse tree represents the same protocol as the original one This opt
43. checked are parsed by the parser Builder and the trees representing the protocol structure are built Hence for illustration we will use the following protocols a b Pax ule Figure 5 1 Basic structure of the checker Compliance Checker Builder gt rond The parse trees representing these two protocols are on Figure 5 2 To find composition errors of a set of n components connected together via their interfaces protocols their parse trees of these components are combined together using the binary consent operator consent operator is applied n 1 times each time one component is composed with the result created so far Using consent operator for component composition enables us to detect three types of errors bad activity no activity and infinite activity The resulting structure i e the parse tree of the composed protocol is used to generate the state space The consent operator itself can detect bad activity and no activity errors As the infinite activity is not a property of a single state this error is detected within the traverser component of compliance checker The strategy used for traversing the state space is known as Depth First Search Should an error bad no or infinity activity be detected the traversing is stopped and the checker reports to the user the error type found and an error trace describing the problem found 31 Implementation Figure 5 2 Parse trees for a b and a
44. cols julia ProtocolControllerMixin 4 2 Environment controller For the purpose of automated generation of environment for primitive Fractal components it is necessary to have an in memory representation of the application architecture and other environment related in formation namely i the name of the Java class which works as a container for sets of values for method parameters ii optionally Java code for user defined stubs and drivers iii simplified version of component s frame protocol describing environment s behavior also optional and iv mapping between names of Fractal interfaces and names of classes that work as stub implementations of the interfaces As in the case of static and runtime checking we use the runtime representation of an ap plication just before starting To associate environment related information with every primitive component we have created an environment controller with the following interface public interface EnvironmentController Returns the name of a class with value sets 4 String getFcValueSetsClass Assigns a name of the class with value sets to a component pri void setFcValueSetsClass String valueSetsClass 16 New features developed within this project Returns the Java code for user defined stub y String getFcUserStubCode Assigns Java code for user defined stub to a component SI void setFcUserStubCode Stri
45. components At runtime a protocol is associated with a component using the protocol controller that holds the protocol In order to use this settings it is necessary to customize the Fractal runtime to attach a protocol controller to newly created components The way a protocol controller is attached to a component is specific to a particular Fractal implement ation In the case of Julia this is achieved by modifying the Julia configuration e g the julia cfg file in the following way Protocol Controller interface protocol controller itf protocol controller org objectweb fractal behprotocols ProtocolController Protocol Controller implementation protocol controller impl org objectweb fractal julia asm MixinClassGenerator ProtocolControllerImpl Checking compliance on the tree of instantiated components allows us to uniformly support both applications built from ADL as well as ap plications built directly from code as described in Section 6 2 40 User s manual org objectweb fractal julia BasicControllerMixin org objectweb fractal behprotocols julia ProtocolControllerMixin Protocol Controller added to primitive component kind primitive interface class generator component itf binding controller itf super controller itf lifecycle controller itf name controller itf protocol controller itf component impl container binding controller impl super controller impl lifecycle co
46. ctweb fractal julia asm InterceptorClassGenerator org objectweb fractal julia asm LifeCycleCodeGenerator org objectweb fractal behprotocols julia RuntimeCheckInterceptorCodeGenerator org objectweb fractal julia asm MergeClassGenerator optimizationLevel 6 4 3 Running a runtime checked application To make a Fractal application subject to runtime checking the only step to be taken is to include the customized Julia configuration file in the list of configuration files to be processed The command below shows how the HelloWorld example is launched from Ant except for setting the classpath The most significant difference is the additional configuration file added to the julia config system property in addition the verbosity of the runtime check framework is increased for demonstra tion purposes java Dfractal provider org objectweb fractal julia Julia Djulia loader org objectweb fractal julia loader DynamicLoader Djulia config etc julia cfg etc julia rtcheck cfg Dfractal protocols rtcheck verbosity 2 org objectweb fractal behprotocols adl Launcher WrappedHelloWorld r The runtime check framework can be configured via properties the properties are ractal proto cols rtcheck recordtrace fractal protocols rtcheck stoponerror fractal protocols rtcheck throwerrors fractal protocols rtcheck re corderrors and fractal protocols rtcheck verbosity The properties control whether the runtimecheck framework record
47. ding builder attrigute builder implementation builder Rrotocokbuilder implementation builder ehviroboment builder component builder component builder binding builder binding builder attribute builder attribute builder protocol builder protocol builder environment builder lenvironment builder 4 4 Interceptors While extending Fractal and Julia with support for runtime checking of compliance of component be havior with the specified protocol we have encountered a number of issues some of which have required modifications to Julia In this section we describe the Fractal and Julia extensions we developed to support the runtime checking In principle runtime checking is achieved by introducing an interceptor for each business interface of the component being checked on each event method entry or exit this interceptor notifies the runtime check controller introduced into the controller part of the component This controller creates an instance of the runtime checker backend with the specified protocol and notifies the checker backend of each such event In case the checker detects that the event violates the protocol the error is recorded op tionally the application may be notified by throwing a ProtocolViolationException The typical interaction among these parts is shown in the sequence diagram in Figure 4 4 21 New features developed within this project Figure 4 4 Sequence diagram capturing inte
48. e and memory consuming process therefore we provide the developers with both run time checker and the checker for code analysis and they should be seen as complementary to each other More details on code analysis of primitive components are presented in Chapter 3 Section 4 7 1 and Section 4 7 2 Chapter 2 Behavior protocols overview 2 1 Events and traces Events are the keystone of behavior protocol semantics Every event is atomic We define two types of events requests and responses Let m be the fully qualified name of a method Then m stands for a request call of m and m stands for a response return from m Always two components cooperate on an event one component emits the event and another component absorbs the event To distinguish between those two roles we use the prefix for emitting and for absorbing If m is a method name the symbols m m m m are called event tokens Recall Figure 1 1 from Section 1 2 1 In the protocol of Client log log would stand for emitting the call of log 10g while log 1log would stand for absorbing the return from log 10g To specify that an event occurs as an internal event of a component C i e it results from a communic ation of C s subcomponents we use the prefix To provide a way to specify a request and the corresponding response at once we define abbreviations if m is a fully qualified name of a method m is an abbreviation for the protocol m
49. e which is the case In the rest of this chapter we show an overview of verification tasks which can be done with behavior protocols Detailed description of behavior protocols can be found in Chapter 2 1 2 2 Static checking Using the static behavior protocol checker two important properties of component behavior can be analyzed statically i e at the development time composition errors and behavior compliance To explain what a composition error is let us assume that the behavior protocol of the Client com ponent from Figure 1 1 changed in the following way log log log log log close Le Client does notcall log open at the beginning However Logger expects open to be called as the first one In general an attempt of a component A to call a method of another component B in a situation where the call is not expected by B i e such a behavior of B is not specified in B s beha vior protocol is called bad activity of A Bad activity is one of composition errors as it results from composition of components with incompatible behavior protocols Other types of composition errors are described in Section 2 4 2 The basic idea of behavior compliance is that for a composite component C the behavior of its intern als determined by joint behavior of its subcomponents S1 Sn should be compliant with the be havior specified by C s protocol Figure 1 2 Example of a composite component with behavior protocols
50. e checker should be launched with the option action test the frame protocol aIN m bIN m eop events which the components communicate through aIN m bIN m eop another protocol aIN m b s aOUT m b u a s aOUT m a u b s aIN m b u aOUT m aIN mS b u b s aIN m b u aOUT m b u fevents aOUT m a s a u Ds b u eop fanother protocol bIN m a s bOUT m a u b s bOUT m b u 58 User s manual a s bIN m a u b s bOUT m b u a S a u y eop events bOUT m eop another protocol aOUT m bOUT m eop there are no unbound operations close the empty list with eop eop Note that you should get a bad activity error when checking these protocols 6 4 Fractal extensions Run time checker 6 4 1 Getting started Runtime checking is integrated into Fractal by the means of the runtime check controller The runtime check controller closely cooperates with the protocol controller and with runtime check interceptors which notify the controller as method requests and responses pass through the component membrane The runtime check controller is responsible for initializing the interceptors obtaining the protocol set in the protocol controller and creating an instance of the runtime checker backend implementation The easiest way to apply runtime checking to an application is to star
51. e than one event a simple event or an atomic action in a single step which causes the consent operator not to be associative when applying to behavior protocols containing atomic actions In other words the result of the com position depends on the order the components are composed together 27 New features developed within this project 4 6 Checker enhancements 4 6 1 Static checking 4 6 1 1 Incomplete bindings The behavior protocol checker is able to detect incomplete bindings Section 2 4 3 If a set of operations of unbound interfaces is given to the checker the methods on provides interfaces are supposed not to be called and in the case a method of an unbound required interface is called the checker detects and reports the unbound interface call error This type of error is detected on the top level i e the place of the last use of consent and the time requirements are therefore acceptable There is no command line option for turning the detection of unbound requirements off instead an empty set of these oper ation can be passed as the last parameter in order not to check for incomplete bindings 4 6 1 2 Collection interfaces In Fractal a component type is a list of interface types Every interface type specifies in addition to the name signature role and contingency also the cardinality of the interface type singleton or col lection As the interfaces defined by a collection interface type are created laz
52. eeee een eeneees 29 4 7 1 Checker for code analysis ete eee testes e nE ere e esent ve ee ren 29 4 7 2 Extensions to the Java PathFinder esssssss eene 29 Se Implementation 20 5 5 Lee Ln es petere te Set gere EE ss 31 5 1 Behavior protocol checker static version esses IH meme 31 5 1 1 Implementation overview 2 2 0 0 eee eee ec cece ence HI HI HI eI emm emer hee rene 31 3 1 2 Basic structure and interaction 5 n eee i tet teet Eee tte iE Rear ERE kae s 32 2311 3 Optimiz tions ess ere eee e Ee ERE epe ee Sees by rte eroe rp eite e ere ee ede 33 5 1 4 The composition and conformance test sssssssssssse ee eee 33 lil Component Reliability Extensions for Fractal component model 5 1 5 Visualization 5 steed dete terere Peste beer Ere dioe oper EER EEN CUPRUM Eo Ute Y 34 3 1 6 Further information aeos ese o EP cedere I et 36 5 2 Implementation of the runtime checker 0 ccc cece eee cence ee ceeeea e emen 36 5 2 ONCT VIEW cuo ri eer b gerer b RE HE RR Ue ES quss Pte abi even pep el 36 3 272 ALONG B CHOTIS os ones ie eo eee Ree roe be een s pute cor e Reste PR CO sh Sexe o Eo UE e sep E eR UNE br 37 25 2 3 Implementation details os ete d eto nds tee Sete Perte e eise ene OR ER RC 37 5 3 Cooperation of Java PathFinder with protocol checker 37 3 3 HC hecker Tor code an lysis ie M RR ei eee erus 37 5 3 2 Extensions to the Java Path
53. emo compon ents There are minor differences between protocols for static and runtime checking In the runtime protocols we had to remove the numbered suffixes from method names e g TokenIn validated_1 or TokenInvalidated_2 for methods where they were required for static checking The suffixes are used to distinguish processing of several parallel calls of the same method As they all represent a single method in the implementation the Julia interceptor will know only the method name without a suffix when passing it to the runtime checker As the core of the runtime checker is the same as the core of the static checker which does not interpret the method suffixes 1 e TokenInvalidated 1 and TokenInvalidated 2 are simply two different methods for the static checker core the runtime checker would not be able to match a method name from the interceptor without suffix to a method name from a static behavior protocol with suffix This is the reason why we had to remove the suffixes and to create the separate runtime protocols Another feature used in static procotols are atomic actions In the protocols for demo components they are used to specify the synchronization behavior for some methods and to distinguish the initial ization stage and running stage of components as these two behaviors are much more easy to describe and comprehend with atomic actions As an atomic action requires that all the methods it contains are processed at the s
54. epServer component needs to be extended to accept two calls of IDhcpCallback IpAd dressInvalidated in parallel Figure 6 9 DhcpServer composite component behavior protocol IDhcpCallback IpAddressInvalidated IDhcpCallback IpAddressInvalidated IManagement UsePermanentIpDatabase IIpMacPermanentDb GetIpAddress IManagement UsePermanentIpDatabase IManagement StopUsingPermanentIpDatabase IManagement StopUsingPermanentIpDatabaseS Now the compliance check can be rerun and after several seconds of computation the user obtains a positive result In the case when a composition error is found the checker can be run with visualization option to obtain both the parse tree graph and state space transition graph java jar checker jar action visualizedot f compliance bp The output of the visualization process is the dot format see Section 6 3 3 for details Note that visualization only makes sense when the order of magnitude of the state space size does not exceed hundreds as larger state spaces are not handled properly by the dot tool 6 3 1 4 Checking for incomplete bindings If we consider the example from the Section 6 3 1 2 and Section 6 3 1 1 we know that IIpMacPerman entDb requires interface should be an optional interface and therefore does not need to be bound to another interface We denote the methods of this interface as unbound unbound ops IIpMacPermanentDb Ge
55. er backend is in an accepting state To properly address there requirements we have put the responsibility to manage the lifecycle of the RuntimeCheckController to the life cycle controller in Julia this is realized via the class RuntimeCheckLifeCycleMixin to be included in the lifecycle controller object The set Fc Started method of this mixin obtains the protocol configured for the component from the Pro tocolController and uses this protocol to initialize the RuntimeCheckController The setFcStopped method stops the runtime check controller which verifies that the protocol permits to stop Figure 4 7 Declaration of interface RuntimeCheckController public interface RuntimeCheckController public void enterFcMethod String itfName String methodName boolean isClient Object params public void leaveFcMethod String itfName String methodName boolean isClient Object params public String getFcCurrentMethods public String getFcMethodHistory public void startFcRtcheck String protocol public void stopFcRtcheck 4 4 3 Handling protocol violations An important issue to decide is what action should the runtime checking system take when it detects a protocol violation In such a situation it is already known that the application violates the protocol specified for the particular component but that may not be a sufficient reason to terminate the applic ation Instead i
56. erence between the standard and static variant is that the standard variant directly instantiates and runs the components while the static variant generates Java code which when executed performs all the instantiation and execution steps The Java and static Java backend work the same way only they do not use Fractal API to instantiate and run the components they rather instantiate the components as ordinary Java classes Our approach to behavior checking relies on having runtime information about components structure and protocols associated with them which is not easily possible with the Java backends The use of the static Fractal backend does not make a good sense for static checking of protocol compliance Thus we have decided to support only the standard Fractal backend We have extended the backend to handle a protocol element by calling set FcProtocol method on the protocol controller associated with a respective component and to handle an environment element by calling setFcValueSetsClass setFcUserStubCode setFcUserDriver sCode setFcProtocol and setFcItfStubs methods on the environment controller associated with a respective component The architecture of the extended backend is shown in Figure 4 3 20 New features developed within this project Figure 4 3 Fractal ADL backend with support for a protocol and an environment backend ype builde type builder implementation builder type builder omponent builder bin
57. est only using the consent oper ator i e the first protocol is not inverted in this case but it is composed together with the other pro tocols Again the protocols are composed in a backward order action a visualizedot the checker will create the files for the dot visualization tool representing the parse trees and the automaton that would be used in the compliance check In this case the first protocol is supposed to be the frame protocol and is therefore inverted before visualization verbosel v level there are 3 levels of verbosity 0 not verbose default 1 normal verbose mode 2 extremely verbose mode useful for debugging The program will according to given verbose level print out information about each step of the compliance test or visualization process and at the end also prints out the length of the test in milliseconds 56 User s manual nomultinodesl m disables the multinode optimization performed while parsing the input protocols Option can be useful for benchmarking reasons noexplicitl e disables the conversion of subautomata to the very fast explicit automata Option can be useful for benchmarking purposes noforwardcutl f disables the forward cutting optimization which eliminates those transitions in the resulting automaton that would be discarded by the use of restriction operator Option can be useful for benchmarking purposes Note that when using the consent opera
58. ew log open log close i e to start by calling log open twice and Client behaved in compliance with this protocol so that no protocol violation would be detected by the run time checker for Client error would be reported for Logger as its protocol does not allow to accept a call of the Log open method twice 2 6 Code analysis The purpose of code analysis of a primitive component is to check whether the component s behavior is bounded by its frame protocol that means checking whether the component can accept and emit method calls on its frame interfaces only in sequences that are determined by its frame protocol Main advantage of code analysis over runtime checking is that all techniques of code analysis are exhaustive i e they check all the possible runs of the verified code We decided to employ model checking which is one of the more popular techniques of software code analysis see Chapter 3 We show the idea of code analysis on the example from Figure 1 1 in Section 1 2 1 Assume that the frame protocol of Client is defined in the same way as in Section 1 2 1 i e it is log open log log log log log close and that the implementation of C1ient in Java is with only fragments presented public class Client private Logger log public void run log open log log message 1 log log message 2 if some condition log log message 3 log close public static void main St
59. fg Besides introducing the new controller this file also extends the definition of the lifecycle controller This additional functionality implemented 59 User s manual in the Runt imeCheckLifeCycleMixin class initializes the runtime check controller at the time the component starts and notifies the runtime check controller when the component stops To properly handle identity aware interceptors the configuration file also introduces a new base class for the inter ceptor objects BasicIdentit yAwareComponent Interface The key elements of the config uration file are shown in Figure 6 10 60 User s manual Figure 6 10 Controller descriptor extensions defined in julia rtcheck cfg interface class generator org objectweb fractal julia asm InterfaceClassGenerator org objectweb fractal behprotocols julia BasicIdentityAwareComponentInterface 4 Runtimecheck Controller runtimecheck controller itf runtimecheck controller org objectweb fractal behprotocols RuntimeCheckController Runtimecheck Controller implementation runtimecheck controller impl org objectweb fractal julia asm MixinClassGenerator RuntimecheckControllerImpl org objectweb fractal julia BasicControllerMixin org objectweb fractal julia control name UseNameControllerMixin org objectweb fractal behprotocols julia BasicRuntimeCheckControllerMixin lifecycle controller impl org objectweb fractal julia asm MixinClas
60. for each primitive component in ADL 69 User s manual We demonstrate the code checking framework on a sample component application involving the Client and Logger components Section 1 2 1 Complete implementation of the example can be found in the examples logger directory As for Julia it is necessary to add a configuration file that supports both the protocol and environment controllers Section 6 5 2 to the julia config system property and to turn on storing generated classes to a temporary directory viathe julia loader gen dir system property Storing classes generated by Julia on disk is necessary for model checking of Fractal components with Java PathFinder to work More specifically it is because of our re implementation of Java classloaders for JPF via its MJI abstraction Section 5 3 2 which assumes that classes generated by Julia are stored on disk and not only in memory The ADL of the example available also in the file LoggerDemo fractal is the following lt definition name logger LoggerDemo gt lt interface name run role server signature java lang Runnable component name client gt interface name log role client signature logger Log gt interface name run role server signature java lang Runnable content class logger ClientImpl lt protocol value run run log open log log log log log close gt lt environment gt lt valuesets classname l
61. g Section 1 2 3 1 and code analysis Section 1 2 3 2 1 2 3 1 Run time checking The main motivation for developing the run time checker is the run time verification of a primitive component However in principle the run time checker can be used also for a composite component The run time checker keeps track of the method calls on external interfaces of a component at run time and checks whether the behavior of the component is bounded by its protocol The main disadvantage of this approach is that unlike the static checking it is not exhaustive even if the behavior of a primitive component is not bounded by the protocol it may not become evident for many runs of the component application monitored by the run time checker More details on run time checking and the differences between static and run time checking are presented in Section 2 5 1 2 3 2 Code analysis The checker for code analysis verifies whether the behavior of a primitive component is bounded by the behavior protocol of the component The verification is done statically i e at the development time and is based on the analysis of the component code It is exhaustive i e if the behavior of the component is not bounded by the protocols it is always detected if the analysis completes On the Introduction other hand the code analysis is an undecidable problem in general i e the analysis may not stop for some inputs Even if it stops it is a very tim
62. i runs JPF with the checker to check whether the component is bounded by its frame protocol 5 3 1 Checker for code analysis At the side of the checker cooperation is implemented by the JPF Traverser class that is able to accept notifications from JPF and by the JPFCooperatingTraverser class that extends the JPFTraverser with support for coordination of backtracking The checker for code analysis works in a way similar to the static checker in each state it generates the list of all possible transitions and moves along one of them The only difference between the static version and this one is that via noti fication of the transition taken in JPF state space JPF chooses the transition to be taken and tells the checker when to backtrack The want sBackt rack method of the JPFStaticChecker returns true only in the cases when the checker is in an already visited state Each time JPF gets into an already visited state it asks the checker for a permission to backtrack If the checker agrees both JPF and checker backtrack otherwise the state space traversal goes on by visiting the JPF already visited states again and visiting unexplored states on the checker s side 5 3 2 Extensions to the Java PathFinder The JPF listener is represented by the ProtocolListener class which implements the Search Listener interface a part of the JPF API The checker receives notifications as method calls on its JPFTraverser instance the object is provided b
63. ied java rtcheck org objectweb dsrg behprotocols demo Token protocol satisfied BUILD SUCCESSFUL Total time 17 seconds In order to demonstrate the runtime checker we prepared another version of the FlyTicketClassifier that does not call the IAfFlyTicketDb GetFlyTicketsByFrequentFlyerld method as it should the beha vior protocol describing its correct behavior remains the same as in the previous example with correct implementation of FlyTicketClassifier component The runtime checker will then detect the incorrect component implementation To run the demo with the faulty FlyTicketClassifier go to the demo proto directory andtype ant check runtime fail The output of the checking is the following especially note the rtcheck FlyTicketClassifier checker is already stopped due to error s found message of the runtime checker full listing is in a separate file TXT http kraken cs cas cz ft doc demo Listing check runtime fail txt ant check runtime fail ava rtcheck CardCenter protocol satisfied ava rtcheck AccountDatabase protocol satisfied ava rtcheck Firewall protocol satisfied ava rtcheck Arbitrator protocol satisfied ava rtcheck FlyTicketClassifier checker is already stopped due to error s found java Erroneous events 1 recorded for component FlyTicketClassifier ava IFlyTicketDb GetFlyTicketsByFrequentFlyerId ava Trace 5 of 5 recorded for component FlyTicketClassifier ava
64. ily their names are in general not known at compile time However behavior protocols can specify only the traffic on the interfaces with known names Therefore the checker supports only singleton interfaces and collection interfaces with names known at compile time 4 6 1 3 Multiple bindings Handling multiple bindings basically means to replace interface names in frame protocols as described in Section 4 5 1 This is implemented by parsing the frame protocols and replacing parts of the parse trees 4 6 1 4 Atomic actions Atomic actions Section 4 5 2 are handled by the checker as standard actions the binding of an atomic action has the same time requirements as the binding of standard actions as there may be only one single action inside an atomic action that can be bound on a single component binding 4 6 1 5 Substantial performance improvements Since its first version a lot of new features have been added to the behavior protocol checker They include state space and parse tree visualization consent operator atomic actions runtime checking and the Fractal interface Although the implementation of new features has required substantial changes to the code of checker resulting into a more complex and more time consuming application the per formance has actually improved by implementing a new state representation and a faster state space generation aglorithm As the checker uses on the fly state space generation a suitable and
65. imization can be easily performed at this point without any loss of parsing speed while saving both the time and the space needed later during the checking After composing all the input protocol parse trees via the consent operator a composition and protocol compliance check can be performed 32 Implementation 5 1 3 Optimizations Before the protocol checking is performed other optimization is done building explicit 1 e pregen erated automata for small parse subtrees this sometimes enhances the speed of the subsequent checking Because cycles and forward edges may appear in the transition graph of the automaton the use of a global state cache improves the checking speed since states may be visited and walked through more than once The problem arising with the use of such a global state cache is again caused by the size of state space in some cases it can be simply impossible for all the states visited so far to fit into the cache because of the limited amount of memory available The solution used here is to forget some of the states being stored in the cache when the cache size exceeds a specified size This of course decreases the checking speed but the performance is still better than in the case of not using the global cache at all The variant of the DFS algorithm with forgetting states from the global cache is called Depth First Search with Replacement DFSR 5 1 4 The composition and conformance test As ment
66. inding content attributes controller template controller protocol environment gt lt ATTLIST component name CDATA REQUIRED definition CDATA IMPLIED lt ELEMENT protocol EMPTY gt lt ATTLIST protocol value CDATA REQUIRED gt lt ELEMENT environment valuesets userstub userdriver protocol itfstub gt 18 New features developed within this project lt ELEMENT valuesets EMPTY gt lt ATTLIST valuesets classname CDATA REQUIRED gt lt ELEMENT userstub EMPTY gt lt ATTLIST userstub file CDATA REQUIRED gt lt ELEMENT userdriver EMPTY gt lt ATTLIST userdriver event CDATA REQUIRED file CDATA REQUIRED gt lt ELEMENT itfstub EMPTY gt lt ATTLIST itfstub name CDATA REQUIRED classname CDATA REQUIRED gt The Fractal ADL framework has been built as a component based application This allows us to easily extend it with new features such as handling the protocol and environment elements The top level architecture is shown in Figure 4 1 It divides responsibilities to the loader which parses the ADL the compiler which checks its validity and processes it and to the backend which builds the application being described by the input ADL Our modification to the Factory are denoted by red color we have added interfaces for handling protocol and environment declarations to the compiler and the backend component Figure 4 1 Fractal ADL fact
67. ioned above a test basically means searching for an error state causing a compliance violation of the given protocols In the process of traversing the state space the comparison of states is necessary Since the automaton i e the states and transitions to other states is generated on the fly the compar ison of states via comparison of their references simply doesn t work Therefore the approach of state signatures representing the internal structure is used here A state signature represents both the shape the structure of the corresponding parse tree and the position in it For example the state of the automaton representing the protocol a a b bS when the trace having been traversed is a a has the signature 1100 denoting the path from the root node to the leaf a The second digit of the signature 1 expresses that the second action has been already performed As the state of each simple automaton i e automaton accepting exactly one word e g a is represented by a single bit both state comparison based on these signatures and their management is very fast and compact The position within the state space is represented by an instance of the class St ate see Figure 5 5 In general for each node of the parse tree we construct a finite automaton generating the language represented by the corresponding subtree of the parse tree starting in this node The state of such an automaton consists of the states of the automa
68. itions of behavior compliance pragmatic compliance published in PV02 and consensual compliance which uses the consent operator AP05 and is im plemented in the current version of the behavior protocol checker 2 4 2 Composition errors Composition errors are communication errors which result from composition of components with in compatible behavior If the definition of the components is enhanced by behavior protocols those composition errors can be checked statically The first type of composition error is bad activity which was demonstrated in Section 1 2 2 It occurs when a component A tries to call a method of a component B in such a way which in not specified in B s behavior protocol No activity or deadlock occurs when computation in a component application can not progress none of the components is able to emit an event and at least one of the components has not finished its computation the application thus cannot stop correctly To show an example of no activity let us modify the frame protocol of Client s A subcomponent from Figure 2 1 in Section 2 3 Behavior protocols overview logl open logl log logi close Here the B component will be blocked as it expects a call of the not i y method on its nt 2 interface this call is never emitted by A After A makes all the calls specified in its behavior protocol a no activity error occurs An infinite activity divergence occurs when computatio
69. l basic operators cssssssssseseeeeee eene eene hee ee hene hene rhe nes 7 2 3 Frame and architecture protocols tette teet ane tere Ere Ee ERO ER e ERR EEEE E 7 244 Static checking onec eee tre err recenter neon prede E ve deep p dress erue ive ey see Eee dosi TET 9 24 1 Protocol Compl ance oni nte ree rtr TATE ES EE SEE e reri rer ie Pere ER ERES 9 2 1 2 COMPOSITION ETTOFS cis ies dees cet een eerie iir Seuss ER RR Er eer Eee NER E Re eb MEE eeu 9 2 4 3 Incomplete bindings etr rto D treo het E co RUE y PORTER 10 2 5 Run time checkimg eR IDA VIRIS Rena ne erede 11 2 6 Code analysis prsesia ee Er cr re SEE TE E ER ERROR QE ERE RR ERI RS 12 3 Model checking of software components 0 eee eee cece sec ee eens ce eee emen hen enm enm e mener eene 14 3 LS Environment sosie Em 14 3 2 Java PathEinder it nete tert eee sie ror pete e eerte Segel EEEE E 15 4 New features developed within this project sssssssssesssesseseee e e emm em e He men enne rene 16 4 1 Protocol controller treten eene eee Woodend eres get eevee eed 16 4 2 Environment controller sissors rettet et t rete veto e peak eet ey aee Ere eR ses Pa ve Er tete ss 16 4 3 Extensions to Fractal ADL eemper III epe eee Re rr Ee ipee 17 AA Interceptors 3 3 oe et err C RR rer Dr RS ERE EC PER EIS CERE REECPRR REEF AEO EORR XE EA PET 21 4 4 1 Identity aware interceptors ssssssssessseeseee eee nemen eee hee ee hne en hhe nennen
70. llback RequestNewIpAddress IDh cpListenerCallback RenewlpAddresst IDhcpListenerCallback ReleaseIpA ddress IDhcpCallback IpAddressI ck IpAddressInvalidated NU e IManagement UsePermanentIpDa Protocol Synchroops Protocol Build start Protocol RequestNewIpAddress IIpMac Callback RenewIpAddress IDhcpLis DhcpCallback IpAddressInvalidated NULL IDhcpCallback IpAddre ssInvalidated NULL IManageme IManagement StopUsingPermanentIp Build finished Build finished State space estimate 824 Optimizing the parse tree for the composition test done created with capacity of 2112000 items created with capacity of 2147483647 items Cache Cache 1024 Stack 024 tack 024 tack 024 tack 024 Stack uorneunmpcdmw size size size size size 51 51 51 2l EDT 1979 states visited Protocols are composition error free OK Taken 1 seconds Permanen Ce nt Da nvalidated NULL IDhcpCallba iL IManagement UsePermanentIpDatabas tabaseS IDhcpListenerCallback tDb GetIpAddress IDhcpListener nerCallback ReleaselpAddress I StopUsingPermanentIpDatabase tabase Now the user can create behavior protocol describing the composite component DhcpServer 48 User s manual Figure 6 6 DhcpServer composite component behavior protocol IDhcpCallback IpAddressInvalidated
71. lt B J C K gt x The rest of the protocols is transformed in the classical way 4 5 2 Atomic actions 4 5 2 1 Overview Atomic actions AA are a behavior protocols construct allowing cooperating components to synchron ize They have been added to behavior protocols as a consequence of component synchronization problems which arised during the work on specification of the Airport Internet Access Application components Although in some cases the behavior of a component may be described using behavior protocols without AA a version using AA are usually not only much easier to construct but also more readable afterwards Furthermore using AA behavior protocols correspond with component imple mentation in a more straightforward way As an example of a behavior protocol containing an atomic action enclosed in square brackets and consider the following example IDhcpController Start IListenerController Start IListenerController Start IDhcpController Start 4 5 2 2 Syntax An atomic action may occur in a behavior protocol at positions where a single event and an abbreviation may Atomic action starts with and ends with There is a coma separated list of events the use of abbreviations is not allowed as their use doesn t make sense here between and 4 5 2 3 Semantics Basically an atomic action is treated as a single event i e it is supposed to be executed in a single step An atomic actio
72. ly useful since by default JPF checks the target program only for deadlocks uncaught exceptions and assertions JPF also provides the MJI Model Java Interface abstraction which allows to execute certain methods in the underlying host VM instead of the JPF VM this can be used to reduce the state space size Use of the MJI abstraction is especially required in the case of native methods which cannot be executed in the JPF VM Chapter 4 New features developed within this project 4 1 Protocol controller In order to allow for the static and the runtime checking of a Fractal based application it is necessary to have an in memory representation of the application architecture and the protocols associated with its particular components For this purpose we use the runtime representation of an application as it is just before starting At this point all components are instantiated in memory but not running thus their structure can be queried using content controllers and binding controllers To associate a protocol with every component we have created a protocol controller with the following interface public interface ProtocolController Returns the frame protocol associated with a component Xy String getFcProtocol Assigns a frame protocol to a component y void setFcProtocol String protocol We implemented this controller for Julia in the form of a mixin class org object web fractal behproto
73. lysis also for the purpose of reducing time and space requirements of the checking process therefore there are two versions of the Simulator component one for runtime checking in the SimulatorRun source file and one for code analysis in the SimulatorJpf source file the proper one being selected during compilation and copied to the Simulator java file 72 References PTA Mach M Plasil F Kofron J Behavior Protocol Verification Fighting State Explosion Published in the International Journal of Computer and Information Science Vol 6 Number 1 ACIS ISSN 1525 9293 pp 22 30 Mar 2005 BCS Bruneton E Coupaye T Stefani J B The Fractal Component Model Draft 2 0 3 February 5 2004 http fractal objectweb org specification PV02 Plasil F Visnovsky S Behavior Protocols for Software Components IEEE Trans Software Eng 28 11 1056 1076 2002 AP05 Adamek J Plasil F Component Composition Errors and Update Atomicity Static Analysis Journal of Software Maintenance and Evolution Research and Practice 17 5 Sep 2005 AP04 Adamek J Plasil F Partial Bindings of Components any Harm Presented at the SACT 2004 Workshop Busan Korea held in conjunction with the APSEC 2004 conference and published in the Proceedings of APSEC 2004 IEEE Computer Society ISBN 0 7695 2245 9 pp 632 639 Nov 2004 CGP Clarke E Grumberg O Peled D Model Checking MIT Press Jan 2000 JPF
74. ment The picture shows both provided server interfaces shown as solid black rectangles and required client interfaces shown as solid white rectangles of the components and also bindings between them The bindings are shown as arrows going in the direction of method calls Each arrow in the picture actually represents a method call or method binding so only the whole bunch of such arrows leading from one interface to another represents the binding between the interfaces It can be deduced from the picture that the inner IpAddressManager component is bound the outer interfaces IManagement provided interface type IIpMacPermanentDb required interface type this interface does not need to be bound and IDhcpCallback required interface type of the DhcpServer composite component The DhcpListener primitive component is bound to the IpAddressManager component via the IDh cpListenerCallback interface This example is a simplified version of the DhcpServer composite component from the Demo The components that are missing in this simple example are in fact considered to be inside the IpAddress Manager component presented here At this level of abstraction the IpAddressManager component can be simply viewed as a black box with its provided and required interfaces and defined behavior and one does not need to worry about the real composite nature of the component implementation 6 3 1 2 Writing protocols First we want to check the compli
75. n is in one of the two states enabled or disabled It can be executed in the enabled state only An atomic action is enabled in the current state if and only if for each accept event an event starting with in the atomic action there exists a component in the composition able to emit the corresponding request event in the current state If there s not a component able to emit a request event corresponding to an accept event of the atomic action the atomic action is disabled The corresponding accept and request events yield as in a common case a tau action consider the following protocol fragment ma mc consent ma 2welsma ime s The application of the consent operator to behavior protocols containing atomic actions may result in a protocol containing the bad activity composition error This situation arises in the following case The atomic action contains no accepting event an event starting with i e it contains internal and emitting events events starting with and respectively only and there s an emit event in the atomic action that is not accepted in the current state by any component in the composition 4 5 2 4 Notes For each two components combined via the consent operator there may be at most one event inside of an atomic action that is also contained in the set of synchronization events for these two components This requirement reflects the fact that a component cannot perform mor
76. n of a component application never stops but components are never blocked i e always there is an event which can be both emitted and absorbed Figure 2 2 Example of infinite activity interface Notification void notify ntp notify tntr notify ntp il ntp T ntr Intr notify FB ntp notify Intr notify Anexample of a component composition resulting in infinite activity can be found on Figure 2 2 Here the A and B components call forever the not ify method on each other s nt p interface in turns More information on composition errors can be found in APO5 2 4 3 Incomplete bindings We say that a component architecture has incomplete bindings if there exists an interface either provided or required which does not participate in any binding we call such an interface an unbound interface The existence of an unbound interface is not necessarily a design error this typically happens when the designer reuses a component developed originally for different application and decides to utilize only a part of the component s functionality If the behavior of the components in the architecture is specified using behavior protocols it is possible to statically check whether the incomplete bindings cause a problem An unbound provided interface can cause bad activity or no activity Section 2 4 2 On the other hand an unbound required interface can cause a new type of composition error unbound requires error Un
77. nce One of the behavior properties which can be statically verified with our behavior protocol checker is compliance of an architecture protocol PA of a component C with the frame protocol PF of C Informally there are two conditions which have to be satisfied in order for PA to be compliant with PF let F be the frame of C 1 PA specifies acceptance of any sequence of calls of the methods provided by F that are dictated by PF 2 For such sequences PA specifies only such calls of the methods required by F that are anticipated by PF Example of an architecture protocol not compliant with the frame protocol was already described in Section 1 2 2 As a more elaborate example of compliant behavior recall the architecture protocol of Client from Figure 2 1 in Section 2 3 lt A logl log gt open lt A ntl B nt2 gt notify B 1og2 log 1log lt A logl log gt log lt A logl log gt close and the corresponding frame protocol log open log log log log log close The architecture protocol is compliant with the frame protocol because if we abstract from the internal events of C1ient which are not important from the point of view of compliance and from different naming conventions the architecture protocol uses binding names the frame protocol uses interface names both the protocols specify the same set of traces or in this particular case the same trace We have developed two different formal defin
78. nd envir onment declarations 17 New features developed within this project We have extended the Fractal ADL by adding elements protocol and environment as children of definition and component elements The following code shows an example of architecture definition written in the extended ADL the extensions are highlighted in bold lt definition name LoggerDemo gt lt component name client gt interface name log role client signature logger Log gt content class logger ClientImpl protocol value log open log log log log log close environment valuesets classname logger LoggerEnvValues gt lt environment gt lt component gt lt component name logger gt interface name log role server signature logger Log gt content class logger LoggerImpl protocol valuez log open log log log close environment lt valuesets classname logger LoggerEnvValues gt lt environment gt lt component gt lt binding client client log server logger log gt lt definition gt To be precise we have changed the Fractal ADL DTD in the following way lt ELEMENT definition interface component binding content attributes controller template controller protocol environment gt lt ATTLIST definition name CDATA REQUIRED extends CDATA IMPLIED 2 lt ELEMENT component interface component b
79. nd the MJI native peers for them are not distributed with JPF As the functionality provided by those classes is necessary for Fractal and Julia to work we had to re implement the classes and provide corresponding MJI native peers in order to enable checking of programs that use the Fractal API with Java PathFinder In particular we had to extend JPF with support for class loaders and file I O Additionally we also extended Java PathFinder with support for modeling time 38 Chapter 6 User s manual This chapter illustrates typical scenarios of using the protocol checker The structure of this chapter follows the two main ways a component application is being built 1 e using Fractal ADL vs building an application directly and how a protocol is associated with a component The last part of the chapter is dedicated to using the protocol checker as a standalone tool independent of the Fractal component model 6 1 Fractal ADL protocol checking 6 1 1 Getting started The easiest way of checking the compliance of component frame protocols in Fractal is to augment the Fractal ADL of an existing application to contain frame protocol definition Recall the example from Section 1 2 1 shown in Figure 6 1 Figure 6 1 Example of a component application with behavior protocols interface Log void open void log String message void close log Client log open log open Hog log log log log log Hog cl
80. ng userStubCode Returns the map of event names to Java code for user defined drivers jp Map getFcUserDriversCode Assigns a map of event names to Java code for user defined drivers to a component ef void setFcUserDriversCode Map userDriversCode Returns the protocol describing the behavior of the environment not the inverted frame protocol Er String getFcProtocol Assigns a protocol describing the behavior of the environment to a component Ny void setFcProtocol String pro Returns a map of Fractal i EOGOl nterface names to names of manually created stub implementation classes Ep Map getFcItfStubs Assigns a map of Fractal interface names to names of manually created stub implementation classes Er void setFcItfStubs Map itfStubs We implemented this controller for Julia web fractal behprotocols julia in the form of a mixin class org object EnvironmentControllerMixin 4 3 Extensions to Fractal A DL As discussed in Section 4 1 and Section 4 2 we associate a frame protocol with each component of an application and also some environment related information with each primitive component of an application Thus to enable the users to use Fractal ADL for describing the architecture of Fractal applications we had to extend the Fractal ADL syntax to accommodate the frame protocol a
81. ntroller impl name controller impl protocol controller impl org objectweb fractal julia asm InterceptorClassGenerator org objectweb fractal julia asm LifeCycleCodeGenerator org objectweb fractal julia asm MergeClassGenerator optimizationLevel 6 2 Building application directly from code 6 2 1 Associating a protocol with a component instance When an application is built directly from Java code protocols are assigned to components by calling the method set FcProtocol on the protocol controller associated with a component This is illustrated in the following code snippet which shows how a protocol is set for the Logger component Protocols of the other components in the application are assigned in the same way not shown in the example Component boot Fractal getBootstrapComponent GenericFactory cf Fractal getGenericFactory boot Component logger cf newFcInstance loggerType primitive ProtocolController loggerProtoCont ProtocolController logger getFcInterface protocol controller loggerProtoCont setFcProtocol log open log log log close 41 User s manual 6 2 2 Checking instantiated components The checking of protocol compliance is performed on an instantiated component application before it is started using its lifecycle controller The checker is invoked by calling static method check on the class org objectweb fractal behprotocols staticchecker ProtocolChecker The checker
82. ogger LoggerEnvValues gt lt environment gt lt component gt lt component name logger gt interface name log role server signature logger Log gt content class logger LoggerImpl protocol value log open log log log close gt environment lt valuesets classname logger LoggerEnvValues gt lt environment gt lt component gt lt binding client client log server logger log gt lt binding client this run server client run gt protocol value run run gt lt definition gt The classname attribute of the valuesets element denotes the class that provides sets of values to be used as method parameters by the generated environment In our example the Logger Logger EnvValues class is used for this purpose The process of code checking can be started with the command ant check code which first creates or cleans the temporary directory where the class files generated by both Julia and the environment generator are stored and then starts the Fractal ADL launcher with the following command 70 User s manual java Dfractal provider org objectweb fractal julia Julia Djulia loader org objectweb fractal julia loader DynamicLoader Djulia config etc julia cfg output dist etc julia proto cfg Djulia loader gen dir tmp V Xmx256M org objectweb fractal behprotocols adl Launcher checkjpf tmp logger LoggerDemo Notice that it is necessary to pa
83. ompliant with its protocol There are two reasons 1 B can emit its call B log2 log gt 1og before open is called by A or after close is called by A and 2 the calls of the 1og method emitted by A and B can occur in parallel None of these situations is permitted by the behavior protocol of Client The construction of the protocol describing behavior of C1ient s internals was shown only for illus tration In practice this is done automatically by the behavior protocol checker Also in the situation when components in a group communicate with each other it is not possible to use the parallel oper ator to specify the resulting behavior more advanced operators have to be used instead see Chapter 2 1 2 3 Verifying behavior of primitive components For a primitive component i e a component that is directly implemented in Java instead of being composed of several subcomponents the behavior compliance Section 1 2 2 cannot be verified by the static checker Section 1 2 2 The reason is that the static checker requires the behavior of both the component and its internals subcomponents implementation to be specified by behavior protocols and it can therefore verify the compliance for composite components only There are two ways to verify whether the implementation of a primitive component is compliant with the protocol or as we say in this context whether the component s behavior is bounded by the protocol run time checkin
84. ory with support for a protocol and an environment org objectweb fractal fractalprotocols fractaladl Factory loader loader backend type builder type builder implementation builder implementation builder component builder t component builder binding builder HEN binding builder attribute builder fF attribute builder protocol builder protocol buider environment builder environment buider We have modified the compiler component by adding subcomponents for processing the protocol and environment declarations and passing it to the backend The Figure 4 2 shows the extended compiler component 19 New features developed within this project Figure 4 2 Fractal ADL compiler with support for a protocol and an environment compiler ompiler type huilde emientation builde component buitder binding build r ribute bdilder protocoMbuilde primitive compilers environm nt bwildey primitive compilerO primitive compiler1 primitive compiler2 primitive compiler3 primitive compiler4 primitive compiler5 primitive compiler6 attribute compiler compiler builder environment compiler compiler builder Fractal ADL allows for different backends The choice of a backend influences how a resulting com ponent application is built As for now there are four different backends available Fractal static Fractal Java and static Java Fractal and static Fractal use Fractal API to instantiate and run components The diff
85. ose log close The example consists of two components The right one implements a logger The left one implements a client which uses the logger The protocol of the Logger component prescribes that first the log maintained by the logger has to be opened by calling the method void open then arbitrary number of log entries can be written by calling the method void log String message Eventually using the log is completed by closing the log calling the method void close The introduction of behavior protocols does not change how an application is implemented Only the Fractal ADL architecture definition here the file LoggerDemo fractal has to be augmented with the protocol specification as shown below the lines specificying the behavior are marked with bold font This file along with a sample implementation of the components can be found in directory ex amples logger definition name LoggerDemo gt interface name run role server signature java lang Runnable component name client interface name log role client signature logger Log gt interface name run role server signature java lang Runnable content class logger ClientImpl protocol value log open log log log log log close lt component gt 39 User s manual lt component name logger gt interface name log role server signature logger Log gt content class logger LoggerImpl
86. protocol and incorrect end component stops when not permitted by the protocol The first kind of error is demonstrated on the c1ientWrap per component The erroneous protocol r run r run s print asks for a nested call of r run before issuing s print The error is reported by a ProtocolViolationException The second kind of error can be observed in the top level component WrappedHelloWorldIncorrect where the erroneous protocol r run r run r run requires that the method r run is called at least twice The error is reported at the time the demo stops by printing message protocol does not permit to stop here By experimenting with configuration of the runtime check framework via properties the various ways to handle an error can be observed The alternative ADL file WrappedHelloWorldIncor rect fractal may be easily launched with the command ant Drun parameters WrappedHelloWorldIncorrect r execute 64 User s manual 6 4 4 Case Study Applying runtime checker on the Airport internet lounge demo To demonstrate the runtime checking on a non trivial case study we have used the implementation of the airport internet lounge demo described in the Demo description http kraken cs cas cz ft doc demo Demo Description pdf technical details of the implementation are described in the separate document Demo _ implementation notes http kraken cs cas cz ft doc demo ftdemo html We assigned runtime protocols to all d
87. protocol describes only sequences of method calls on the component s interfaces abstracting from the values passed as method parameters and return values Such a level of abstraction is very suitable for verification tasks specific to software components Introduction 1 2 1 Behavior protocol basics Figure 1 1 Example of a component application with behavior protocols interface Log void open void log String message void close log llog open log open llog log log log log log llog close log close On Figure 1 1 there is an example of a component application consisting of two simple components The component Logger provides basic logging functionality which is used by the component C1ient Therefore Client s required log interface is bound to Logger s provided 10g interface Logger s 10g interface consists of three methods open which has to be called at the beginning of the logging session 10g which can be called several times after the open method was called every call of the 1og method causes writing of the string passed as the message parameter into a persistent store and the close method which has to be called at the end of the logging session Ina classic software development process description of a component s functionality such as Logger has typically the form of a plain English text which is not suitable for an automatized behavior veri fication To fill this semantic gap
88. r class which are used by some components from the Demo As 71 User s manual these components assume that the fields of the Simulator class are set to meaningful values at runtime it is necessary to initialize those fields also for the purpose of code analysis with the Java PathFinder The userdriver element contains the event attribute which denotes a protocol event and the file attribute which denotes the file with Java code that is used to indirectly invoke the event The concept of user drivers is useful especially for components which invoke some methods on their required interfaces as a reaction to some outer world events an example of such a component is the Dh cpListener component Files representing user stubs and drivers for the Demo are available in the demo env stubs and demo env drivers directories respectively In addition to defining environment related information in ADL and providing user defined stubs and drivers we had to create stub implementations of several components from the Demo which are ref erenced by fields of the Simulator component All these stub implementations belong to the org objectweb dsrg behprotocols demo env package Main purpose of these manually created stubs is to bring down the requirements on CPU time and memory that are necessary for code checking of primitive components with Java PathFinder Moreover we had to create a special imple mentation of the Simulator component for code ana
89. raction in the runtime check subsystem RuntimeCheckinterceptor RuntimeCheckBackEnd InterfaceObject RuntimeCheck Controller Com ponentlm pl Actor LI event r1 I l I l L3 I I I 4 4 1 Identity aware interceptors The Julia interceptor framework features several Interceptor generators Of these the SimpleCode Generator at the first sight seems to perform the task required by the runtime checking extensions deliver a method call to a controller whenever a method call starts or completes and also provides the interface name However SimpleCodeGenerator canonly provide the name of the language type used by the interface or a possibly configurable string which can however only depend on the language type of the interface and cannot provide the concrete name of the interface This difference is particularly obvious when a component features multiple interfaces based on the same language type Furthermore Julia originally did not provide a way to configure an interceptor such as to provide it with getter setter methods to set configuration properties as it was not possible to specify an interface to be implemented by an interceptor and it would not be possible to call such a method without the use of reflection The first enhancement to Julia was to allow an interceptor generator to specify Java interfaces to be implemented by the generated interceptor class For a class generator this had already been possible by overriding
90. re 4 5 Declaration of interface IdentityAwareInterceptor public interface IdentityAwareInterceptor public ComponentInterface getFcItfInstanceRef public void setFcItfInstanceRef ComponentInterface itfRef public String getFcItfInstanceName public void setFcItfInstanceName String newlItflnstanceName public void setFcItfIsClient boolean itfIsClient public boolean getFcItfIsClient The interceptor code generator is responsible for providing implementations of these methods In the case of the Runt imeCheckInterceptorCodeGenerator provided in our framework these methods are generated via the ASM toolkit the method implementations are simple accessor getter set ter methods for the respective local private attributes Please note that we have been also considering an alternative approach instead of generating the methods for each interceptor class these methods might also be inherited from a common base class However the current Julia interceptor framework does not permit selecting the base class of an inter ceptor and it is not feasible to make it configurable without significantly changing the structure of component descriptors Additional issue related to the introduction of identity aware interceptors into Julia was assigning the responsibility to initialize the interceptors While it was originally considered that this task would be done by the newly introduced Runt imeCheckCont roller controller
91. ring args Logger log new Loggerimpl Client client new Client client setLog log client run 12 Behavior protocols overview It is clear from the example above that the implementation of Client is not bounded by the protocol as the implementation allows three invocations of 10g 10g in some cases whereas the protocol allows only two invocations Since the code analysis via model checking is an exhaustive verification technique it will find the error when it checks the run in which the condition in the if statement evaluates to t rue and con sequently 1og 10g is called for the third time 13 Chapter 3 Model checking of software components Model checking CGP is a formal method of verification of finite state systems The basic idea is that a model checker checks whether the model of a target system satisfies the property expressed in some property specification language The checking is done by traversal of the state space that is generated from the model Some model checkers accept as input the model manually created by the user while others are able to automatically extract the model from the source code However both approaches have severe drawbacks Manual construction of the model is a tedious and error prone process On the other hand automated extraction of the model faces the problem that the model is an abstraction and therefore it may represent behavior not possible
92. rotocols P Q standsfor P P Q EO 2 3 Frame and architecture protocols From the point of view of behavior every component can be divided into two parts frame and archi tecture The frame of a component C consists of all interfaces which are provided or required by C to outside world the components which are external to C The architecture of C consist of frames of C s direct subcomponents and bindings between those frames and also bindings between interfaces of C s subcomponents and interfaces of C itself Behavior protocols overview Figure 2 1 Example of a composite component with bindings among subcomponents interface Notification void notify M Client log1 open Int1 notify tlog1 log log1 close tlog2 log log open log log log log llog close On Figure 2 1 the frame of Client consists of the only log interface while its architecture is formed by the frames of A B and the bindings A logl lLog gt lt B log2 log gt lt A nt1 B nt2 gt as explained in Section 1 2 2 in the context of the Client component A 109g1 10g stands for the binding of the Log interface of the A subcomponent to the 10g interface of Client itself here we introduce lt A nt1 B nt2 gt the binding between interfaces of A and B subcomponents An architecture is always associated with a concrete frame we also say that the architecture implements this frame Following
93. rror values when a violation of the component s protocol is detected If true or false default t rue false the erroneous event is ignored and checking resumes from the current position in the state space fractal protocols rt sets whether an exception should be thrown when a protocol check throwerrors values violation is detected true or false default false fractal protocols rt sets the level of output on stderr produced by the check verbosity values 0 1 runtimecheck subsystem 0 no output 1 only protocol viola 2 or 3 default 1 tions 2 report on controller initialization and successful com pletion 3 report on event processing 4 5 Extensions to protocols 4 5 1 Multiple bindings In Fractal any interface can participate in more than one binding if this is the case we say that the interface has multiple bindings As behavior protocols were originally developed for a component model where every interface can have at most one binding this alternative did not come into question when the algorithm for architecture protocol construction was designed Therefore the algorithm had to be revisited for Fractal Let C be a component whose subcomponents S1 Sn have the frame protocols F1 Fn The classical construction of C s architecture protocol not considering multiple bindings is done in two steps In the first step the interface names in the frame protocols F 1 Fn are replaced by the binding n
94. s a part of the GraphViz package see http www research att com sw tools graphviz The dot tool supports multiple format output for example EPS PNG or VRML and is thus very flexible If the switch action visualizedot is given to the checker the program creates several files those with names starting with pt_ contains parse trees description and those with names starting with a contain automata transition graph For simplicity of the graphs the nodes of a parse tree are not labeled with the operator names but with the following symbols instead adjustment operator t alternative operator and parallel operator complement operator amp composition operator consent operator DET determinization operator EXPx explicit automaton is used here corresponding protocol is printed below the parse tree es intersection operator or parallel operator ie repetition operator 57 User s manual restriction operator sequence operator The subtrees of the parse tree that are replaced in the consequence of Explicit Automata Optimization with explicit automata for the compliance test are shown as gray pentagons and the corresponding protocol i e the expression generating the language being accepted by this automaton is printed out below the parse tree as the graph legend 6 3 4 Example of protocol input file Hash sign denotes comments As the first protocol is a frame protocol th
95. s the complete trace of the component execution what behavior is desired when an error occurs throw a ProtocolViolationException logthe error and continue execution whether the component should log all errors encountered and what level of verbosity is desired The properties and their default values are described in detail in Section 4 4 4 62 User s manual We demonstrate the runtime check framework on an example based on the Fractal ADL HelloWorld demo We have augmented the demo with behavior protocol specifications in addition we have wrapped the client and server components into composite components clientWrapper and serverWrapper The ADL of this demo available in the file WrappedHello World fractal is also shown in Figure 6 11 Figure 6 11 ADL specification of the HelloWorld demo lt definition name WrappedHelloWorld gt interface name r role server signature java lang Runnable component name clientWrapper gt interface name r role server signature java lang Runnable interface name s role client signature Service component name client gt interface name r role server signature java lang Runnable interface name s role client signature Service content class ClientImpl protocol value r run s print gt component binding client this r server client r binding client client s server this s gt protocol value r
96. sGenerator LifeCycleControllerImpl org objectweb fractal j org objectweb fractal julia UseComponentMixin org objectweb fractal julia control lifecycle BasicLifeCycleCoordinatorMixin org objectweb fractal julia control lifecycle BasicLifeCycleControllerMixin to check that mandatory client interfaces are bound in startFc org objectweb fractal julia control lifecycle TypeLifeCycleMixin to notify the encapsulated component if present when its state changes org objectweb fractal julia control lifecycle ContainerLifeCycleMixin extensions for runtimecheck controller interaction require a reference to ProtocolController org objectweb fractal behprotocols julia UseProtocolControllerMixin require a reference to RuntimeCheckController org objectweb fractal behprotocols julia UseRuntimeCheckControllerMixin do the interaction org objectweb fractal behprotocols julia RuntimeCheckLifeCycleMixin ulia BasicControllerMixin Cisse Cs 61 User s manual primitive interface class generator component itf binding controller itf super controller itf lifecycle controller itf name controller itf protocol controller itf runtimecheck controller itf component impl container binding controller impl super controller impl lifecycle controller impl name controller impl protocol controller impl runtimecheck controller impl org obje
97. same ap plication as for demonstration of the runtime checking framework i e the implementation of the airport internet lounge demo For the purpose of code analysis we had to define certain environment related information for each primitive component in ADL More specifically we had to define the so called user stub for each primitive component and in the case of the DhcpListener component we also had to define several so called user drivers All these definitions are stored inside the environment element in addition to the valuesets subelement Moreover we also had to provide a simplified version of component s frame protocol as a specification of environment s behavior for several primitive components e g Arbitrator in order to make checking of these components feasible with respect to CPU time and memory require ments In such a case the environment is generated from the simplified frame protocol of the target component but checking is still done against the original frame protocol The purpose of user stubs and user drivers is to extend the generated environment of a component with the functionality of the Simulator class Section 6 4 4 since we check the primitive components one by one and therefore it is not possible to use the Simulator class in the same way as in the case of runtime checking The userstub element contains the f ile attribute which denotes the file with Java code that initial izes certain fields of the Simulato
98. simply go to the demo proto directory and type ant check runtime The most important part of the checking output is the following full listing can be found in a separate document TXT http kraken cs cas cz ft doc demo Listing check runtime txt ant check runtime 66 User s manual java rtcheck CardCenter protocol satisfied java rtcheck AccountDatabase protocol satisfied java rtcheck Firewall protocol satisfied java rtcheck Arbitrator protocol satisfied java rtcheck FlyTicketClassifier protocol satisfied java rtcheck AfDbConnection protocol satisfied java rtcheck CsaDbConnection protocol satisfied java rtcheck FrequentFlyerDatabase protocol satisfied java rtcheck Timer protocol satisfied java rtcheck DhcpListener protocol satisfied java rtcheck TransientIpDb protocol satisfied java rtcheck IpAddressManager protocol satisfied java rtcheck ValidityChecker protocol satisfied java rtcheck Timer protocol satisfied java rtcheck ValidityChecker protocol satisfied java rtcheck Timer protocol satisfied java rtcheck ValidityChecker protocol satisfied java rtcheck Timer protocol satisfied java rtcheck FlyTicketDatabase protocol satisfied java rtcheck DhcpServer protocol satisfied java rtcheck org objectweb dsrg behprotocols demo Token protocol satisfied java rtcheck org objectweb dsrg behprotocols demo Token protocol satisf
99. so complex that the static checker cannot be used Last but not least run time checker can be used to check the compli ance of a primitive component behavior with the frame protocol this cannot be done using the static protocol checker in principle because there are no subcomponent frame protocols We show the functionality of the run time checker on the example from Figure 1 1 in Section 1 2 1 The frame protocol of Client specifies that the Log 10g method has to be called after Log open has been called If log close were called instead at that moment the run time checker would detect an error What exactly happens when such an error is detected depends on the configuration of the run time checker Typically the error is reported and logged within the runtime checking framework The run time checking framework may throw an exception in the calling thread to notify the application about the erroneous call or the application may continue without being affected In either case the run time checking of the component whose frame protocol was violated is stopped It is not possible to con tinue run time checking of the component in this case as the behavior protocols formal model does not support error recovery The run time checker also detects the violation of the frame protocol caused by the component s envir onment the outer world For example if the frame protocol of Client were log open 11 Behavior protocols overvi
100. ss the Launcher class two additional arguments check jpf which turns code checking with JPF on and the path to the directory for generated class files tmp in the example followed by the definition of the target component When checking the Logger example via the ant check code command the output may take the following form java Checking implementation of primitive components with JPF java Checking component client java Component client OK tmp client Output txt java Checking component logger java Component logger OK tmp logger Output txt There are two lines of text printed for each primitive component in the hierarchy First the text Checking component lt component s name gt is printed before the checking of the component actually starts Then after the checking of the component is completed the text Component component s name OK ERROR name of file with details is printed The OK message is printed only if no errors were found during checking otherwise the ERROR message is printed In both cases the name of file with details is displayed in brackets next to the OK ERROR message We decided to store detailed output like error traces number of states etc in a separate file as the output can be quite complex 6 5 4 Case Study Applying code analysis on the Airport internet lounge demo To demonstrate the code checking framework on a non trivial case study we have used the
101. system 5 2 3 Implementation details The runtime checker class provides two methods a method for notification about the event being performed and a method testing whether the current state is accepting i e whether the protocol allows the component to finish The class also remembers the current state the initial state is set in the con structor and each time the notify method is called this state is updated Should an event not allowed by the protocol occur the notify method returns bad activity information 5 3 Cooperation of Java PathFinder with protocol checker As already said in Section 4 7 the cooperation between JPF and the checker is implemented via i a JPF listener that notifies the checker of invoke and return instructions corresponding to method calls on frame interfaces of a checked component and ii an enhanced JPF search engine that differs from the standard search engine in that it asks the checker for a permission to backtrack when JPF comes to an already visited state In this section we describe the modifications of JPF and the checker necessary to successfully implement the JPF listener and the enhanced JPF search engine The main entry point is the JPFChecker class Its check method accepts an instantiated root Fractal component and then for each primitive component in the hierarchy i uses the environment generator to generate an environment of the component from its frame protocol ii configures JPF and ii
102. t is a provides interface or must not be performed if it is a requires interface otherwise causing an unbound requires called error 6 3 1 3 Checking for compliance After the protocols are completed their compliance check can be performed For the example above the command line would be java jar checker jar action testconsent f architecture bp The output of this command should be OK If the user wants more detailed information the static behavior checker can be run with the verbose option java jar checker jar action testconsent verbose 1 f architecture bp The output of the checker is then a bit more complex as can be seen in the following listing The im portant parts of the output i e the number of states visited and the result of the protocol checking are highlighted in bold 47 User s manual Protocol Synchroops Callback Protocol 2IDhcpl RenewlpAddress IDhcpListe Build finished Protocol Build start IDhcpListenerCallback RequestNewIpAddress IDhcpListenerCallback nerCallback ReleaseIpAddress RenewlpAddress ID Build start ListenerCallback k RenewlpAddress IDhcpLis IDhcpListenerCallback RequestNewIpAddress IDhcpListener hcpListenerCallback ReleaselpAddress RequestNewIpAddress IDhcpListenerCallbac tenerCallback ReleaseIpAddress IDhcpCal lback IpAddressInvalidated NULL IDhcpCallback IpAddressInval idated NULL IDhcpListenerCa
103. t may be useful to collect more information on this application failure such as collecting 24 New features developed within this project the subsequent events observable on the interfaces of the faulty components The default behavior is to log and report the error including the execution trace so far collected for the component and also the current stack trace optionally a runtime exception ProtocolViolationException may be thrown to inform the application that the attempted call is not permitted by the protocol Here please note that raising the exception prevents the method call from actually occurring when the erro neous event detected is a request event but obviously cannot prevent the call in the case of a response event The error handling policy can be configured via JVM properties described in the following section 4 4 4 Technical notes The runtimecheck subsystem may be configured via the following JVM properties fractal protocols rt sets whether the runtime check controller should record all er check recorderrors values roneous events true or false default true fractal protocols rt sets how many recent events should be kept to aid with locating check recordtrace values the source of an error Special values 1 unlimited storage 1 O or a positive integer default 1 and 0 no events recorded fractal protocols rt sets whether runtime checking should stop for a component check stopone
104. t the application augmented with behavior protocol specifications in the same way as described in Section 6 1 1 the only additional step required is to activate the runtime check controller framework which is achieved by modifying the controller descriptors used for primitive and composite components please see Section 6 4 2 We demonstrate this on a modified version of the Fractal ADL HelloWorld example augmented with simple behavior protocols This example is available in the examples helloworldadl directory The example can be started via the protocol aware Fractal ADL launcher org object web fractal behprotocols staticchecker Launcher The Ant build file provided with this example allows us to start the demo simply by issuing the com mand ant execute The program output includes the in this configuration verbose output from the runtime checking framework which reports on the protocols applied to the components and the results of the checking Configuring the behavior and the level of output of the runtime check framework will be discussed in detail in Section 6 4 3 6 4 2 Julia configuration To activate the runtime checking framework is is necessary to extend the controller descriptor of both primitive and composite components with the definition of the runtime check controller implemented by the BasicRuntimeCheckControllerMixin class The modified controller descriptor definitions are provided in the file julia rtcheck c
105. ta of the node s children nodes enriched with information from this node The information added in the node depends on the node type For example for A1 ternativeNode the piece of information would be the index of the subtree that represents the branch being currently traversed only one branch is traversed at a time in this case 33 Implementation Figure 5 5 The State class hierarchy signature Signature label String cycleStart boolean cycleid long timestamp long acceptingReachable boolean cycleTrace String signaturelnit boolean create State equals another State boolean getSignature Signature compareTo o Object int createSignature ompositeState states State IndexState states State index int As mentioned above there are various types of nodes within the parse tree The node type corresponds to the operator used in the protocol The node class hierarchy is depicted on Figure 5 6 The node is responsible for computing the transitions from the state of the automaton corresponding to that node testing the state for being accepting and providing the initial state of the automaton The algorithms for computing the transitions from the transitions of subautomaton or subautomata in some cases are straightforward in most cases Figure 5 6 The TreeNode class hierarchy TreeNode nodes TreeNode lt lt create gt gt TreeNode protocol S
106. tain both behavior protocols and a specification of actions method calls via which the IpAddressManager first protocol and the DhcpListener second protocol components are bound together Because the components are bound together only by the IDhcpListenerCallback inter face the RequestNewIpAddress RenewIpAddress and ReleaseIpAddress methods from the IDh cpListenerCallback will be the only actions written in the behavior checker input file In this step we don t want to check for incomplete bindings so the unbound operations in the input file will be empty The corresponding input file for the behavior checker may take the form 45 User s manual Figure 6 5 Static behavior checker input file DhcpListener IDhcpListenerCallback RequestNewIpAddress IDhcpListenerCallback RenewIpAddress IDhcpListenerCallback ReleaselpAddress eel eop Synchro ops IDhcpListenerCallback RequestNewIpAddress IDhcpListenerCallback RenewIpAddress IDhcpListenerCallback ReleaseIpAddress eop IpAddressManager IDhcpListenerCallback RequestNewIpAddress IDhcpListenerCallback RenewIpAddress IDhcpListenerCallback ReleaselpAddress IDhcpCallback IpAddressInvalidated NULL IDhcpCallback IpAddressInvalidated NULL IDhcpListenerCallback RequestNewIpAddress IDhcpListenerCallback RenewIpAddress IDhcpListenerCallback ReleaseIpAddress IDhcpCallback IpAddressInvalidated NULL IDhcpC
107. terface Protocol Controller implementation 68 User s manual Environment Controller interface environment controller itf environment controller org objectweb fractal behprotocols EnvironmentController Environment Controller implementation environment controller impl org objectweb fractal julia asm MixinClassGenerator EnvironmentControllerImpl org objectweb fractal julia BasicControllerMixin org objectweb fractal behprotocols julia EnvironmentControllerMixin Environment Controller added to primitive component kind primitive interface class generator component itf binding controller itf super controller itf lifecycle controller itf name controller itf protocol controller itf environment controller itf component impl container binding controller impl super controller impl lifecycle controller impl name controller impl protocol controller impl environment controller impl org objectweb fractal julia asm InterceptorClassGenerator org objectweb fractal julia asm LifeCycleCodeGenerator org objectweb fractal julia asm MergeClassGenerator optimizationLevel 6 5 3 Running the check of primitive components To make a Fractal application subject to code analysis of primitive components it is necessary to 1 configure Julia in a proper way and ii define a frame protocol and environment specific information like name of a class with value sets etc
108. the main method required by JPF Therefore it is necessary to create an environment of the target component and then check the whole program composed of the environment and the component The environment should be generated in a way that forces the model checker to verify all reasonable control flow paths in the component s implementation For that purpose the environment has to i perform all reasonable sequences of method calls on server interfaces of a target component and ii invoke each method several times each time with different values of its parameters We employed a tool for automated generation of environment that was developed outside of the scope of this project As input the tool accepts i the frame protocol of a target component as the behavior specification of the environment and ii the name of a Java class that works as a container for sets of values of method parameters The environment is then generated from the inverted frame protocol AP05 of the target component which is constructed from the frame protocol by replacing all the accept events with emit events and vice versa Our tool also performs several heuristic transformations of the frame protocol before creating the environment in order to minimize the size of the state space of the program composed from the component and environment PP06 Model checking of software components 3 2 Java PathFinder Java PathFinder is a software model checker for Java
109. tlIpAddress eop After running the checker we obtain the error trace Composition error detected missing binding for request IIpMacPermanentDb GetIpAddress SO IDhcpListenerCallback ReleaseIpAddress S1 IManagement UsePermanentIpDatabase S8 IDhcpListenerCallback ReleaselpAddress S9 IDhcpCallback IpAddressInvalidated S16 IDhcpListenerCallback RenewIpAddress 55 User s manual S17 IDhcpCallback IpAddressInvalidated S22 IDhcpCallback IpAddressInvalidated S23 IDhcpListenerCallback RenewIpAddress S24 IDhcpCallback IpAddressInvalidateds S33 IManagement UsePermanentIpDatabase S35 IDhcpListenerCallback RequestNewlIpAddress S40 From the error trace it can be seen that the error is caused by the IIpMacPermanentDb GetIpAddress method called on an unbound interface The problem arises because as the provided IManagement interface is bound the highlighted IManagement UsePermanentIpDatabase event can be performed to enable the use of the external IP MAC address database This implies that the IIpMacPermanentDb required interface can be unbound only if the IManagement provided interface is also unbound unbound ops IManagement StopUsingPermanentIpDatabase IManagement UsePermanentIpDatabase IIpMacPermanentDb GetlIpAddress eop Adding methods of IManagement interface into the list of unbound operations will result into a suc cessful compliance check 6 3 2
110. tor for finding composition errors forward cutting is not applied since the consensual compliance is not based on the subset relation totalmeml t size specifies in MB the size of memory available for the checker data structures Note that the checker needs additional 10 15 MB of memory for the code and the basic data structure that cannot be optimized and that the java virtual machine may allocate more memory if available To restrict the memory allocated use the Xmx option of java virtual machine The default value is 60 cachesizel s size specifies in MB the size of memory dedicated for the state cache This number cannot be higher than the total memory amount The default value is 48 filel f inputfile reads the protocols from the file specified Each protocol and set of synchro op erations has to be ended by an eop token at the beginning of a new line The protocols can be formated using standard whitespace character for better readability protocol lt n gt n th protocol the first is a frame protocol provisions lt n gt synchronization operations for n th and n 1 th protocols unbound operations all operation of unbound interfaces used for detection of incomplete bindings 6 3 3 Visualization As mentioned above the checker is able to create a visualization of the parse trees and the automata that are used for compliance checking The program produces input files for the dot visualization tool that i
111. tput In the following listing the lines in bold highlight the error trace in the protocol note that some actions are decomposed into separate request and response events e g m gt m m The event causing the bad activity is emphasized in italics 52 User s manual Figure 6 8 Input file with highlighted error trace DhcpServer frame protocol IDhcpCallback IpAddressInvalidated IDhcpCallback IpAddressInvalidated IManagement UsePermanentIpDatabase IIpMacPermanentDb GetIpAddress IManagement UsePermanentIpDatabase IManagement StopUsingPermanentIpDatabase 3 0 IManagement StopUsingPermanentIpDatabase Ssynchro ops between frame and architecture protocols IManagement UsePermanentIpDatabase IManagement StopUsingPermanentIpDatabase IIpMacPermanentDb GetlIpAddress IDhcpCallback IpAddressInvalidated eop DhcpListener IDhcpListenerCallback RequestNewIpAddress IDhcpListenerCallback RequestNewIpAddress IDhcpListenerCallback RenewIpAddress IDhcpListenerCallback ReleaselpAddress jy eop Synchro ops IDhcpListenerCallback RequestNewIpAddress IDhcpListenerCallback RenewIpAddress IDhcpListenerCallback ReleaseIpAddress eop fIpAddressManager IDhcpListenerCallback RequestNewIpAddress IDhcpListenerCallback RenewIpAddress IDhcpListenerCallback ReleaselpAddress IDhcpCallback IpAddressInvalidated
112. tring getWeight long getChildren TreeNode changeChild index int newChild TreeNode void forwardCut livingevents TreeSet TreeNode copy TreeNode getLeafCount int getAnotatedProtocol state State AnotatedProtocol getinitial State SequenceNode gt isAccepting state State boolean getTransitions state State TransitionPairs RestrictionNode AdjustmentNode AlternativeNode AndParallelNode CompositionNode ExplicitNode 5 1 5 Visualization The program has also the ability to visualize both the protocol parse trees and their corresponding automata It generates the source file for the dot tool a part of the GraphViz package available at http www graphviz org Names ofthe files containing the description of a parse tree start 34 Implementation with the prefix pt_ and names of files with automata description start with the prefix a_ The dot tool supports a large number of output formats of these EPS and VRML seem to be most useful The files consist of descriptions of nodes and transitions among them while the placement of the nodes and transitions is left up to the dot tool For example to obtain the parse tree diagram shown in Fig ure 5 7 the source file may have the form digraph G size 11 7 Intersection20 label fontname Courier Bold Intersection20 gt Complementi1 Complementl1 label fontname Courier Bold
113. w byte 0 0 0 0 0 0 byte mac2 new byte 0 0 0 0 0 1 Y byte mac3 new byte 0 0 0 0 0 2 InetAddress addrl dhcpListener RequestNewIpAddress macl iLogin LoginWithAccountId addr1 InetAddress addr2 dhcpListener RequestNewIpAddress mac2 InetAddress addr3 dhcpListener RequestNewIpAddress mac3 65 User s manual i Logi n Logi nWithFl yTi cketId addr3 iLogin LoginWithFrequentFlyerId addr2 dhcpListener RenewIpAddress macl addr1 dhcpListener RenewIpAddress macl addr1 dhcpListener ReleaseIpAddress macl addr1 iLogin Logout addr3 dhcpListener ReleaselpAddress mac3 addr3 iLogin Logout addr2 dhcpListener ReleaselIpAddress mac2 addr2 The whole architecture used in the case study is shown in Figure 6 12 Figure 6 12 Architecture of the demo ontroller IFlyTicketDb Je IFlyTicketAuth Account ILifetimeq IFlyTicketDb CardCenter IFlyTicketAuth D 1 1 1 1 1 Ai ICardCenter lArbitratorLifetimeController Arbitrator ICardCenter lArbitratorLifetime AccountDatabase Controller lAccountAuth run amp E 5 E 8 5 T 5 z amp B 5 5 2 g 8 E El x s o AS RS B 3 Fa 5 2 e a Firewall IpAddressManager pi Timer Firewall lipMacTransientDb IListenerLifetime TransientlpDb DhopListener DhcpServer To run the demo with runtime checking
114. with the name of that binding c If P is the name of a provided interface of a subcomponent Sk with multiple bindings C1 11 Sk P gt Cm Im Sk P absorption of a method call on P in the frame protocol of Sk of the form P a is replaced with the protocol T Cl Il1 Sk P a lt Cm Im Sk P gt a In a similar way absorption of a method call of the form P m Q where Q is an arbitrary protocol is replaced with the protocol T Cl 1Il1 Sk P a Q Cm Im Sk P a Q d If R is the name of a required interface of a subcomponent Sk with multiple bindings Sk R C1 Il1 XSk R Cm Im emission of a method call on R in the frame protocol of Sk of the form R a is replaced with the protocol lt Sk R Cl I1 gt a lt Sk R Cm Im gt a In a similar way emission of a method call of the form P a Q where Q is an arbitrary protocol is replaced with the protocol IXSk R C1 I1 5 a Q lt Sk R Cm Im gt a Q e Explicit requests responses on the interfaces with multiple bindings are forbidden Figure 4 8 Example of multiple bindings We demonstrate the rules on the application shown on Figure 4 8 The frame protocol of B of the form J x x is name of a method will be transformed to lt B J C K gt x lt B J D L gt x The frame protocol of C of the form K x will be transformed to 26 New features developed within this project lt A I C K gt x
115. wo inner components the IpAddressManager and the DhcpListener The Dh cpServer works as a component implementation of a DHCP server where the DhcpListener commu nicates with the network clients via the DHCP protocol and the IpAddressManager component is re sponsible for managing the IP addresses assigned to them The key functionality besides being a DHCP server for the local network is to notify other components of disconnected clients after a client s IP address is released via the IDhcpCallback interface The whole DhcpServer component can be managed via the IManagement interface and optionally can use an external database of IP address MAC address mappings the database is accesses via the IIpMacPermanentDb interface Usage of an external database is enabled by the UsePermanentIpDatabase method of the IManagement interface 42 User s manual Figure 6 2 DhcpServer composite component lipMacPermanentDb IDhcpCallback Add Mac Ip Expiration Time IpAddressinvalidated pAddress Remove p GetMacAddress p Mac GetlpAddress Mac Ip GetExpirationTime p ExpTime SetExpirationTime Ip ExpTime lipMacPermanentDb IDhcpCallback DhcpServer IpAddressManager IDhcpListenerCallback IManagement Ip RequestNewlpAddress Mac UsePermanentlpDatabase RenewlpAddress Mac Ip StopRenewingPermanentIpAddresses ReleaselpAddress Mac p StopUsingPermanentlpDatabase LII IDhcpListenerCallback DhopListener IManage
116. y the checker via a call of the getNotifee Note that JPF does not ask for a permission to backtrack in an end state as there is no other way to go on 37 Implementation method of the JPFStaticChecker class In addition to notifications the listener also looks for occurrences of end states in the JPF state space If no end state is visited at all a short warning is printed at the end alerting that there is probably an infinite loop in the code The extended JPF search engine is implemented by the JPFCheckerSearch class that implements the SearchListener interface provided by JPF It is based on the DF Search class also provided by JPF that represents the standard search engine based on DFS As for changes to the core of JPF we modified the POR related code so that a transition is terminated when an invoke or return instruction corresponding to a frame interface method call is executed We implemented it by making such instructions scheduling relevant The list of relevant methods of the frame interfaces of a target component is stored as a static attribute of the JVM class that is a part of JPF it is provided to JPF before it is started in the check method of the JPFChecker class Besides the changes to the JPF core and the extensions related to cooperation we used the MJI abstrac tion for re implementation of several classes from the standard java lang and java io packages because those classes contain some native methods a

Component Reliability Extensions for Fractal component model

Contents

Download Pdf Manuals

Related Search

Related Contents