Monitoring Model Spe i ations in Program Code Patterns Moritz Balz, Mi hael Striewe, and Mi hael Goedi ke Paluno  The Ruhr Institute for Software Te hnology University of Duisburg-Essen, Essen, Germany {moritz.balz,mi hael.striewe,mi hael.goedi ke}s3.uni-due.de Abstra t. Numerous approa hes exist that derive exe utable systems from well-dened spe i ations. However, model spe i ations are not available in program ode of su h derived systems, whi h impedes on- tinuous validation and veri ation at run time. We earlier proposed to embed model spe i ations into well-dened program ode patterns to bridge this semanti gap. We now present an elaboration of our approa h to monitor su h systems at run time with respe t to the underlying ab- stra t models. For this purpose, dierent te hniques are onsidered that allow to a ess the modeling information without relying on additional metadata. Based on this, we present a tool that monitors the exe ution of state ma hines. 1 Introdu tion The reation of software based on formal models is supported by means of various modeling, simulation and veri ation tools. However, urrent te hnologies for model-driven software development (MDSD) ause a loss of semanti information when su h models are transformed into sour e ode by manual or automated ode generation [1℄: The inherent loss of semanti information entails that models are related to derived systems only impli itly [2℄, thus preventing us from being able to monitor the exe ution with respe t to the model semanti s. To bridge this semanti gap, we proposed to embed model spe i ations in obje t-oriented program ode [3℄, for example for state ma hines [4℄. Su h embed- ded models introdu e program ode patterns representing the abstra t syntax of models. This single-sour e approa h allows not only to verify programs at devel- opment time with respe t to the related models, but also to exe ute embedded models at run time by frameworks relying on stru tural ree tion. In this on- tribution we onsider this an opportunity to monitor the exe ution: Sin e these program ode patterns represent model spe i ations ompletely, dierent de- grees of abstra tion are available in the ode at the same time. Hen e we an monitor model exe ution at run time without using other representations than the program ode. At the same time we an observe how models behave with appli ation data. This paper is stru tured as follows: Se tion 2 des ribes the monitoring ap- proa h by introdu ing on epts for embedding and identifying modeling infor- mation in program ode. Then we des ribe dierent possible te hniques to a ess the related program ode fragments at run time in se tion 3. Based on these, a tool for monitoring state ma hines is introdu ed in se tion 4. Afterwards we give an overview of related work in se tion 5 and draw on lusions in se tion 6. 2 Approa h The obje tive of this ontribution is to monitor exe uted software with respe t to high-level spe i ations, but without using additional meta information, so that no in onsisten ies an o ur and the tool hain is as small as possible. While monitoring as a way of verifying the exe ution of software systems at run time is well-established, few approa hes realize veri ation with respe t to formal models the software is based on. The reason, as mentioned in the introdu tion, is that the related spe i ations are not naturally available in the program ode that onstitutes programs at run time: The ode usually des ribes exe ution logi only and not its abstra t semanti s. When it is monitored or veried, the resulting information is generi , fo uses on te hni al details of program ode, or must rely on tra ing metadata to relate the ode to formal models. Considering these problems, we introdu e in this se tion our general approa h of oupling model spe i ations and program ode. 2.1 Embedded Models A monitoring as des ribed above means that the program ode must ontain the spe i ation information. Considering obje t-oriented programming languages like Java, we an observe a trend to in rease the expressiveness of program ode fragments. For example, embedded DSLs [5℄ are domain-spe i languages that are embedded into other languages, so that semanti s of DSLs are used inside a general-purpose language. In addition, some general-purpose languages are able to arry type-safe metadata, e.g., Java Annotations. This enables attribute- enabled programming [6℄ making program ode interpretable even at run time. Embedded models build upon these on epts to relate program ode to ab- stra t spe i ations systemati ally. Ea h embedded model provides a program ode pattern representing the abstra t syntax of a formal model so that a bije - tive proje tion between both exists. The pattern elements rely on the semanti s of the underlying programming language and its expressiveness regarding single fragments and their inter onne tions. The stati al elements of the programming language and their relations are onsidered building blo ks onstituting the pat- tern. They are of interest in our ontext sin e expressiveness of the monitoring depends on their a essibility by appropriate me hanisms at run time. The pattern ode is interpreted by means of stru tural ree tion at run time to exe ute the model spe i ations. Ea h embedded model provides an exe ution framework that a esses and invokes the language elements and thus reates a sequen e of a tions mat hing the related model semanti s. Considering the monitoring, it is essential that the program ode pattern elements and their expressiveness regarding relations to the abstra t spe i ations are by this means a essible at run time. 2.2 Implementation for State Ma hines An instan e for embedded models exists for the domain of state ma hines. Sin e meaningful monitoring in our ontext depends on the availability of model el- ements in the program ode at run time, we will introdu e the program ode pattern here and refer to it later. Figure 1 shows an example ontaining all pro- gram ode stru tures of interest. The lass at the top represents a state; the lass name equals the name of the state. The method in the state lass repre- sents a transition. It is de orated with metadata (the annotation Transition) referring to the target state lass and a  ontra t lass ontaining guards and updates. An interfa e type referred to as a tor is passed to transition meth- ods. Its methods are interpreted as a tion labels whi h an be alled when a transition res. Thus, a sequen e of a tor method invo ations inside a transition method is interpreted as a sequen e of a tion labels for this transition. public class AfterMeasurementState implements IState State Definition { Target State Pointer Contract Pointer @Transition(target = UpUpState.class , contract = BeginUpUpContract.class ) public void beginUpUp(MeasurementModule actor) throws MeasurementAbortedException { actor.doMeasure (); } Transition // ... } Action Label State and Transition Definition in Source Code Contract Definition public class BeginUpUpContract implements IContract< IMeasurementVariables > { Current Variable Values Variable Definitions public boolean checkCondition( IMeasurementVariables vars ) Guard { return (!vars.getAbort() && !vars.getRestart() && vars.getTooLow()); } Update Variable Labels Current Variable Values Cached Variable Values public boolean validate( IMeasurementVariables before , IMeasurementVariables after ) { return ( after.getNumberOfWorkers() == ( before.getNumberOfWorkers() + before.getWorkerDistance()) ); } } Variable Labels Contract Definition in Source Code Fig. 1. A state denition with an outgoing transitions and its ontra t. The rst method of the ontra t evaluates a pre- ondition with respe t to the urrent variable values, while the se ond method evaluates a post- ondition by omparing the urrent values to the previous values. Guards and updates are implemented as two methods in a  ontra t lass whi h is shown at the bottom of gure 1. Both evaluate boolean expressions and return a single boolean value. The guards use the urrent variable values of the state ma hine to determine if a transition is able to re, the updates ompare the urrent values with the values from the point in time before the transition red to determine the hanges to the state spa e. For this purpose both methods a ess a variables type whi h is a fa ade type representing the variables onstituting the state spa e of the state ma hine. This type ontains get methods for ea h variable. The name and return type of ea h method are interpreted as name and data type of the orresponding variable. The exe ution framework interprets and invokes these fragments at run time. The surrounding program ode a esses for this purpose the exe ution framework and passes the lass denition of the initial state as well as the variables and a tor fa ade types as parameters. The state ma hine is then exe uted as follows: 1. The initial state's lass and variables interfa e are passed to the exe ution framework. All states rea hable from the initial state are instantiated. 2. The urrent state is set to the initial state. 3. All transition methods of the urrent state are visited and the variables type instan e is passed to the related guard method to determine if the transition is able to re. 4. The urrent variable values are a hed. 5. The method representing the transition that is able to re is invoked. 6. The urrent variable values and the a hed variable values are passed to the update method for the validation of variable updates. 7. The urrent state is set to the target state of the exe uted transition. The pro ess is ontinued until the urrent state is a nal state or the state ma hine runs into a deadlo k. 2.3 Monitoring at Run Time As an be seen in the state ma hine example, embedded models introdu e pro- gram ode patterns whose elements are related to model spe i ations. The models are thus views on the program ode and need not to be stored in sep- arate notations, so that no in onsisten ies between model and implementation an o ur. Consisten y is not only maintained at development time, but also at run time: Sin e the related ode fragments are not supplementary or optional, but instead used by the exe ution framework, exe uted systems with embedded models arry omplete information about related spe i ations naturally. This availability of models at run time is important for our obje tive to monitor programs with respe t to models, sin e the model views an be extra ted from the ode during exe ution. For this purpose the well-dened elements of the program ode patterns serve as entry points for interpreting and monitoring the program ode. This enables a validation of programs with two purposes: First, the model view itself is of interest for monitoring the model exe ution by the framework, so that inferen es an be made on orre tness of the model from this information. Se ond, embedded models are tightly integrated with arbitrary program ode. This allows for high exibility during implementation, but auses the need to validate orre tness of the surrounding ode with respe t to the model. This is supported with appropriate monitoring sin e the behaviour of the model with appli ation data an be observed. Monitoring of embedded models thus onsiders program ode pattern in- stan es, for example of state ma hines, as well as program ode of the exe ution framework: Sin e it ontrols the exe ution, it is an entry point for a tions to be monitored. Inside the exe ution framework for state ma hines, the following steps an be onsidered:  The exe ution framework iterates on the state ma hine ow until a nal state is rea hed. The urrent a tive state is denoted by a variable inside this iteration pointing to the state lass denition. Changes to this variable must be monitored in order to determine state a tivation.  On e a state is a tivated, the exe ution framework iterates the ontained transition methods. The transition under examination is also denoted by a variable that must therefore be observed.  For ea h transition the exe ution framework invokes the guard and update methods and passes the variables fa ade instan e as a parameter. Of interest are all operations inside this methods, espe ially those that omprise state ma hine variable values. To interpret the guards and updates thoroughly, the omposition of the overall result of these methods from single operation results is also important to monitor. We will now introdu e appropriate monitoring te hniques and afterwards a tool that implements the approa h. 3 Monitoring Te hniques Our obje tive is to use this approa h for monitoring program exe ution with respe t to models at run time, but without arti ial tra ing information. Thus it is important to onsider the a essibility of the program ode patterns and their elements during exe ution. We will introdu e the basi te hnologi al ap- proa hes for this purpose here. While all of them have already been used by other approa hes for monitoring, our ontribution here is the appli ation to program ode patterns arrying the abstra t syntax of formal models. We will therefore not fo us on the general te hnologies, but on their adequa y for monitoring the referen es to model spe i ations at run time, in whi h we en ounter important dieren es. 3.1 Listener Approa h Sin e all information about the running system and the embedded state ma hine semanti s is available inside the state ma hine exe ution framework, the easiest way for monitoring is to extend this framework in order to emit information of interest for monitoring. The exe ution framework is based on stru tural ree tion and a esses and interprets a onsiderable part of the program ode stru tures onstituting the pattern. Besides setting listeners programmati ally, module- based platforms (like OSGi [7℄ in the ontext of Java) allow for a loose oupling of exe ution framework and omponents re eiving information about the exe ution. In the ase of state ma hines, listeners an be notied about events for every operation performed on the embedded model:  Initialization and start of a state ma hine. This in ludes information about all states, transitions and variables as extra ted from the Java ode via ree tion. States are uniquely identied by their fully qualied lass names.  A tivation of states. This indi ates that guard evaluation and transition sele tion in this state will happen subsequently.  Sele tion of transitions. This indi ates that program ontrol will be handed over to the business logi in this transition.  Validation of updates after a transition. The variable values are updated in this event. Additionally, the a hed variable values are supplied to allow for omparisons. Additional information is supplied if the validation failed. When this event is red, program ontrol has been taken over by the state ma hine exe ution framework again. The advantage of listeners is their easy integration into tools based on the Java platform, espe ially in module-based environments. Sin e the listeners are a essible from inside the same Java Virtual Ma hine (provided appropriate programming interfa es or module lookup servi es exist), even self-monitoring of appli ations is possible. Thus an appli ation an gain information about its own exe ution inside the state ma hine. This is possible without on urren y problems sin e the framework passes ontrol of the program ow to the listeners during noti ations, so that all a tions are handled sequentially. While the approa h is working at this level, the degree of detail is limited: Method ontents in Java are not a essible by means of ree tion and thus bla k boxes. For this reason operations inside guards and updates are not visible, but only their results after the related method was invoked by the framework. 3.2 Aspe t-Oriented Approa h Aspe t-oriented programming (AOP) aims to separate ross- utting on erns from business logi . Monitoring and tra ing are often-mentioned examples for AOP usage: Emission of monitoring information is formulated as aspe ts that are woven into program ode. To monitor state ma hine exe ution, the ode stru tures of interest are a essed by point uts. Appropriate advi e written in Aspe tJ [8℄ are shown in listing 1.1. The rst and the third point ut wrap around guard and update methods, invoke them and read the result. Afterwards the monitor is notied about the ontra t lass and the urrent result. The se ond point ut is invoked before a transition method is exe uted, i.e., any method in a lass implementing the IState interfa e. It noties the monitor about the related state lass and transition method name. // Wrap guard method invo ation and notify about the result boolean around(Obje t vars) : exe ution(* IContra t. he kCondition(..)) && args(vars) { boolean result = pro eed(vars); monitor.notifyGuard(thisJoinPointStati Part.getSignature().getDe laringType(), result); return result; } // Notify about forth oming transition method invo ation before() : exe ution(* *.*(..)) && target(IState) { monitor.notifyTransition(thisJoinPointStati Part.getSignature().getDe laringType(), thisJoinPointStati Part.getSignature().getName()); } // Wrap update method invo ation and notify about the result boolean around(Obje t before, Obje t after) : exe ution(* IContra t.validate(..)) && args(before, after) { boolean result = pro eed(vars); monitor.notifyUpdate(thisJoinPointStati Part.getSignature().getDe laringType(), result); return result; } Listing 1.1. The Aspe tJ monitoring aspe t. All points of interest in the program ode pattern are learly identiable by simple rules regarding their lasses and method names, so that point uts an be dened unambiguously. The main advantage of AOP in this ontext is that monitoring an be applied without the need to modify the exe ution framework. With load-time weaving, monitoring apabilities an even be supplemented in systems after the program ode has been ompiled. This allows for exible me hanisms that an be applied depending on the ontext. This is enabled by the fa t that the pattern elements of embedded models are well-known and obligatory: Aspe ts an identify them so that advi e and point uts an address program ode elements related to model elements. Similar as with listeners, this also allows for self-monitoring. However, while this exterior view on the pattern allows for dynami exten- sion of su h software, it prevents full a ess to information of interest: Point uts an handle information regarding the lo ation of program ode in whi h they are exe uted (keyword thisJoinPointStati Part). But, they do not gain a - ess to information in terms of sequen es of point uts: In ea h state, a ertain number of guards is evaluated. Afterwards, one transition method is invoked. While point uts are informed about the single a tions, they annot determine whi h guard belongs to the transition being exe uted; this information has to be guessed or supplemented by interpreting the program ode afterwards. To solve this problem, the exe ution framework ould be hanged to make pointers to the obje ts of interest available as elds. 3.3 Debugging Approa h The debugging approa h delegates low-level observation of the program state to the exe uting platform. The related Java Platform Debugger Ar hite ture (JPDA) [9℄ provides well-dened programming interfa es to a ess related events so that those of interest for our monitoring approa h an be ltered from the event queue. In the ase of embedded state ma hines, state a tivation and transi- tion sele tion are monitored by observing elds ontaining the related referen es in the exe ution framework with Modifi ationWat hpointEvents. For guards and updates, MethodExitEvents are of interest that are triggered after all ode of a method has been exe uted, but before the method is left. We use them to a ess return values of variable interfa e methods when they are invoked. To- gether with information about lo al variable values we an monitor evaluation of guards and updates with su h events, too: Sin e only expressions are used inside these methods, the evaluation is fully omprehensible afterwards by inspe tion of the values of lo al variables. The return value of the method and thus the result of the evaluation is also available in this event. A debugger an hen e a ess all elements of the program ode pattern in model implementations as well as all lo al variables in the exe ution framework. Dierent to the listener and AOP approa hes, this allows for monitoring guard and update method ontents. Sin e all details of expressions are available, the evaluation of guards and updates an be re orded and presented to the devel- oper for ea h step. The debugging approa h is therefore the only one able to a ess all elements of the program ode pattern. A ess to variables and method invo ation results is possible without additional eort when they are a essed by the appli ation itself. For the state ma hine model this is su ient sin e the variables are of interest only when they are evaluated in guards. A debugger would also allow to invoke methods at any time. This ould be of interest for variable methods to determine their urrent value. This is, however, intrusive to the program ow, sin e variable methods may ontain arbitrary business logi , whi h would be exe uted at times not expe ted by the developer. The main inuen e of debuggers, however, is the need for two running in- stan es: The appli ation being debugged and the debugger itself that ontrols exe ution. All information that an be gained is a essible only by the latter, so that a self-monitoring of appli ations is not possible. In addition, debuggers in general have a strong impa t on performan e, so that a monitoring of produ tion systems is urrently not desirable with this te hnology. We thus expe t that this approa h an be used as debuggers are used in general  when the appli ations are validated during development or maintenan e. In this ase the relation to abstra t models is more meaningful than debugging at the sour e ode level only. 4 Monitoring Tool These approa hes enable monitoring of program ode based on embedded models without using tra ing information or other metadata, but by onsidering well- dened ode stru tures only. We will now introdu e a tool that is based on su h approa hes and monitors the related information. Its user interfa e shown in gure 2 ree ts our requirements for the pra ti al use of the monitoring. The graphi al view allows to wat h a tivated state lasses and transition methods. Current and a hed variable values are shown to exhibit the urrent state spa e and to enable monitoring of hanges during transitions. Updates that Fig. 2. A state ma hine model being monitored. Left hand we see the state ma hine with the a tive state and transition highlighted, right hand the variable values onsti- tuting the state spa e. ould not be validated su essfully are listed separately; sin e updates do not have impa t on the program ow, this information allows developers to look for the auses of su h in onsisten ies later on. The state ma hine ow altogether an be paused and resumed by the user. This is possible sin e business logi is invoked during transitions, and exe ution ontrol will afterwards return to the state ma hine. The third button visible on top of the s reenshot noties the exe ution framework that the state ma hine ow should pause after the urrent transition; the button to the right allows then for stepwise exe ution. The tool is realized on the E lipse platform, making it easy to be integrated in E lipse-based development tools. It uses listeners that are loosely oupled over the OSGi servi e registry that is provided by the E lipse platform: Listeners like our tool are hen e OSGi bundles being deployed alongside, but independent from business logi . The listener is registered as a named OSGi servi e that is dete ted by the exe ution framework. The resulting ar hite ture as sket hed in gure 3 allows to use almost arbitrary tools to be notied about events for every operation performed on the embedded state ma hine. 5 Related Work Following our obje tive to monitor the exe ution of program ode that is re- lated to model spe i ations, we must onsider related work with respe t to two Fig. 3. Component ar hite ture with the monitoring listener. Appli ations are om- posed of omponents using the exe ution framework based on the OSGi platform. The listener omponent is optional and hen e only oupled via the servi e registry. topi s: First, general approa hes that relate program ode to high-level spe i- ations whi h are in theory appropriate for monitoring; se ond, the appli ation of monitoring in spe i te hnologi al environments. Round-trip engineering [10℄ relates generated program ode to models but targets the development time instead of the run time and annot be fully auto- mated [11℄. Informal spe i ations an be inferred from program ode by dete t- ing patterns [12℄, and similar, spe i ations an be extra ted from program ode based on design patterns [13℄. However, this requires manual eort or is based on heuristi s and not appropriate for a pre ise monitoring. Exe utable models [14℄ are a essible at run time, too. However, they are only appropriate for ap- pli ations ompletely expressed as models, while we onsider ases where models are onne ted to program ode and thus monitor the related data ex hange. Monitoring for omplian e with so- alled design models [15℄ or design pat- tern ontra ts [16℄ is based on low-level semanti s of detailed patterns. Similarly, model he kers for program ode work with low-level semanti s of the program- ming language and thus onsider whole appli ations as models [17℄. In ontrast, monitoring with embedded models is related to abstra t spe i ations. For this reason it an also learly be distinguished from general debugging approa hes. We do not aim to present a notation for the spe i ation of all possible sys- tem models like the Java Modeling Language (JML) [18℄ or the approa h to use Smalltalk with its introspe tion apabilities as a meta language [19℄. In ontrast to stati analysis tools like Dis oTe t [20℄ we do not target dete - tion of unknown stru tures and models, but fo us on well-known models that an thus be examined more thoroughly and with respe t to a formally-founded ba kground. We also do not require hanges in the program ode to introdu e referen es to spe i ations as is ne essary for PathFinder's veri ation state- ments [21℄ or the approa hes to monitor OCL onstraints with aspe t orientation [22, 23℄, whi h rely on metadata in sour e ode omments. Instead, we an infer all model spe i ations dire tly from the program ode pattern. 6 Con lusion We presented our approa h to monitor model spe i ations that are embedded in obje t-oriented program ode. We were a ting on the assumption that the re- lated program ode pattern stru tures are pre ise enough to allow for inferen e to model spe i ations even at run time. To show this, dierent approa hes for information retrieval have been evaluated as possible alternatives. Our on lu- sion is that all are appropriate to monitor the state ma hine semanti s, although in dierent degree of detail and with dierent impa t on the ne essary hanges to the program ode. All are non-intrusive regarding the sour e ode of the mon- itored system and two of them are even non-intrusive to the sour e ode of the exe ution framework. However, the degree of detail varies sin e only debugging approa hes allow to monitor guards and updates in detail. On the other hand, listeners and AOP require less overhead at run time. With AOP, monitoring aspe ts an even be atta hed dynami ally to the programs sin e they an work on the pattern spe i ations after ompilation. For the urrent implementation of a monitoring tool, the listener approa h was hosen sin e it allows to a ess the most important information with little eort and provides the ability for self-monitoring. However, if the required en- vironment is available, the debugging approa h is more thorough and allows to monitor every detail of the state ma hine exe ution. Future work will thus in- lude the development of an appropriate monitoring tool. Due to the maturity of the JPDA and related user interfa es in integrated development environments, we will then be able to integrate the monitoring with the debugging user in- terfa e of development environments. With this integration, the monitoring of abstra t model spe i ations an be seamlessly integrated with debugging of ar- bitrary Java appli ations, thus making model validation at run time an integral part of the development pro ess. Referen es 1. Brown, A.W., Iyengar, S., Johnston, S.: A Rational approa h to model-driven development. IBM Systems Journal 45(3) (2006) 463480 2. Ti hy, M., Giese, H.: Seamless UML Support for Servi e-based Software Ar hite - tures. In Gue, N., Artesiano, E., Reggio, G., eds.: Pro eedings of the International Workshop on s ientiFi engIneering of Distributed Java applI ations (FIDJI) 2003, Luxembourg. Volume 2952 of Le ture Notes in Computer S ien e., Springer-Verlag (November 2003) 128138 3. Balz, M., Striewe, M., Goedi ke, M.: Continuous Maintenan e of Multiple Abstra - tion Levels in Program Code. In: Pro eedings of the 2nd International Workshop on Future Trends of Model-Driven Development - FTMDD 2010, Fun hal, Portugal. (2010) 6879 4. Balz, M., Striewe, M., Goedi ke, M.: Embedding State Ma hine Models in Obje t- Oriented Sour e Code. In: Pro eedings of the 3rd Workshop on Modelsrun.time at MODELS 2008. (2008) 615 5. Kabanov, J., Raudjärv, R.: Embedded Typesafe Domain Spe i Languages for Java. In: PPPJ '08: Pro eedings of the 6th International Symposium on Prin iples and Pra ti e of Programming in Java, New York, NY, USA, ACM (2008) 189197 6. S hwarz, D.: Peeking Inside the Box: Attribute-Oriented Programming with Java 1.5. ONJava. om (June 2004) http://www.onjava. om/pub/a/onjava/2004/06/ 30/insidebox1.html. 7. OSGi Allian e: OSGi Servi e Platform, Core Spe i ation, Release 4, Version 4.1. IOS Press, In . (2005) 8. Colyer, A., Clement, A., Harley, G.: E lipse Aspe tJ. Addison-Wesley (2004) 9. Sun Mi rosystems, In .: JavaTM Platform Debugging Ar hite ture API http:// java.sun. om/javase/te hnologies/ ore/toolsapis/jpda/. 10. Sendall, S., Küster, J.: Taming Model Round-Trip Engineering. In: Pro eedings of Workshop on Best Pra ti es for Model-Driven Software Development. (2004) 11. Baker, P., Loh, S., Weil, F.: Model-Driven Engineering in a Large Industrial Con- text  Motorola Case Study. In Briand, L., Williams, C., eds.: Model Driven En- gineering Languages and Systems, 8th International Conferen e, MoDELS 2005, Montego Bay, Jamai a, O tober 2-7, 2005, Pro eedings. Volume 3713 of LNCS., Springer (2005) 476491 12. Philippow, I., Streitferdt, D., Riebis h, M., Naumann, S.: An approa h for reverse engineering of design patterns. Software and Systems Modeling 4(1) (February 2005) 5570 13. Mili, H., El-Boussaidi, G.: Representing and Applying Design Patterns: What Is the Problem? In Briand, L.C., Williams, C., eds.: MoDELS. Volume 3713 of Le ture Notes in Computer S ien e., Springer (2005) 186200 14. Hen-Tov, A., Lorenz, D.H., S ha hter, L.: ModelTalk: A Framework for Devel- oping Domain Spe i Exe utable Models. In: Pro eedings of the 8th OOPSLA Workshop on Domain-Spe i Modeling. (2008) 15. Seka, M., Sane, A., Campbell, R.H.: Monitoring Complian e of a Software Sys- tem With Its High-Level Design Models. In: ICSE '96: Pro eedings of the 18th International Conferen e on Software Engineering, Washington, DC, USA, IEEE Computer So iety (1996) 387396 16. Soundarajan, N., Hallstrom, J.O., Tyler, B.: Monitoring Design Pattern Contra ts. In: Pro eedings of the the 3rd FSE Workshop on the Spe i ation and Veri ation of Component-Based Systems. (2004) 8793 17. Holzmann, G.J., Joshi, R., Gro e, A.: Model driven ode he king. Automated Software Engineering 15(3-4) (2008) 283297 18. Leavens, G.T., Baker, A.L., Ruby, C.: JML: A Notation for Detailed Design. In Kilov, H., Rumpe, B., Simmonds, I., eds.: Behavioral Spe i ations of Businesses and Systems, Kluwer (1999) 175188 19. Du asse, S., Gîrba, T.: Using Smalltalk as a Ree tive Exe utable Meta-language. In Nierstrasz, O., Whittle, J., Harel, D., Reggio, G., eds.: Model Driven Engineering Languages and Systems, 9th International Conferen e, MoDELS 2006, Genova, Italy, O tober 1-6, 2006, Pro eedings. Volume 4199 of Le ture Notes in Computer S ien e., Springer (2006) 604618 20. Yan, H., Garlan, D., S hmerl, B., Aldri h, J., Kazman, R.: Dis oTe t: A System for Dis overing Ar hite tures from Running Systems. In: ICSE '04: Pro eedings of the 26th International Conferen e on Software Engineering, Washington, DC, USA, IEEE Computer So iety (2004) 470479 21. Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model Che king Programs. Automated Software Engineering Journal 10(2) (2003) 22. Ri hters, M., Gogolla, M.: Aspe t-Oriented Monitoring of UML and OCL Con- straints. In: Pro eedings of Workshop Aspe t-Oriented Software Development with UML. (2003) 23. Chen, F., D'Amorim, M., Ro³u, G.: A formal monitoring-based framework for soft- ware development and analysis. In: Pro eedings of the 6th International Conferen e on Formal Engineering Methods (ICFEM'04). Volume 3308 of LNCS., Springer- Verlag (2004) 357373