Towards Generic Monitors for Object-Oriented Real-Time Maude Specifications

Towards Generic Monitors for Object-Oriented Real-Time Maude Specifications Antonio Moreno-Delgado1, Francisco Dur´an1, Jos´e Meseguer2 1University of M´alaga, Spain. 2University of Illinois at Urbana-Champaign, United States. {amoreno,duran}@lcc.uma.es,[email protected] Abstract. Non-Functional Properties (NFPs) are crucial in the design of software. Specification of systems is used in the very first phases of the software development process for the stakeholders to make decisions on which architecture or platform to use. These specifications may be analyzed using different formalisms and techniques, simulation being one of them. During a simulation, the relevant data involved in the analysis of the NFPs of interest can be measured using monitors. In this work, we show how monitors can be parametrically specified so that the instrumentation of specifications to be monitored can be automatically performed. We prove that the original specification and the automatically obtained specification with monitors are bisimilar by construction. This means that the changes made on the original system by adding monitors do not affect its behavior. This approach allows us to have a library of possible monitors that can be safely added to analyze different properties, possibly on different objects of our systems, at will. 1 Introduction As system complexity grows, specification of systems becomes an even more important task during the first phases of the software life cycle. With the proliferation of distributed systems due to Cloud-computing systems, Internet of Things, etc., with software being present in all activities of our lives, Non-Functional Properties (NFPs) are gaining relevance in design decisions. Specification of software and its simulation can be used to get insights about how the system is going to behave. Furthermore, by adding monitors or observers to system specifications, software engineers can analyze those NFPs of interest [9]. System specifications have to be instrumented in order to get probes of executions. One may think of different NFPs, such as response time, throughput, mean cycle time or rate of failures. However, different NFPs have to be monitored by different observers, and such observers are typically hard-coded in the specifications. To cope with this lack of modularity, many alternatives have been proposed. For example, in Aspect-Oriented Programming, code is instrumented by monitors as a cross-cutting concern. Other works, as the one presented in [16], propose adding observers as new elements (objects) of the language. See [17] for a discussion of how to monitor non-functional properties in component-based systems. In most cases, and even with more emphasis in the case of distributed or concurrent systems, these specifications are written with, among others, the purpose of verification. Different kinds of verification can be achieved depending on the desired level of evidence and precision in the proofs. Furthermore, some formalisms are more amenable to perform some proofs or checks than others. For example, a specification in Promela/Spin [8] is more amenable to perform model-checking that a specification in UML. Likewise, a specification in Coq [1] is well-suited to perform theorem-proving. This means that a tight dependence between formalisms and the verification one can perform exists. Among all kind of formalisms, we find very attractive those which can be executed, since the software engineers involved in the software development can get insights on where they are failing or on which parts they have to stress. Execution of a system specification means that the system at hand can be simulated in the very first phases of software design, and, at very low additional cost, software engineers can test different designs and approaches, thus getting insight about how the system is going to fulfill the required NFPs. However, to analyze the behavior of a system under simulation, we have to measure the properties we want to study. Rewriting logic [10] provides a formal framework where concurrent and distributed systems can be naturally defined. Since the specification remains within a formal environment, different kinds of verification can be performed: confluence, model-checking, reachability analysis or invariant analysis. Additionally, rewriting logic specifications are executable, providing prototypes that can be simulated and tested. In this work we propose the definition of monitors in a very general way. If monitors are defined following certain guidelines, their addition to any realtime object-oriented specification is automatic, and what more important, the original behavior of the system after being instrumented is not changed. We focus on object-oriented modules that must be defined using Real-Time Maude [14], since the main applications we envision are real-time and stochastic systems. On these specifications, we are interested in measuring system properties, i.e., properties that affect the whole system as throughput, and individual properties, i.e., properties related to concrete objects as traffic or utilization. Monitors can be defined just by querying data. Thus, we give a skeleton Maude module which can be used to define any kind of monitor query by specifying the data structure to use and the query to perform. Besides the theoretical results, a tool in the rewriting logic language Maude is presented to include generically defined monitors to system specifications. Using the reflective capabilities of Maude, we have defined module operations that take the specifications to be analized and the generic monitors to be used on them, and generate new modules with the instrumented specifications. We have used the extensibility capabilities of Full Maude [4, 6] to provide a new module expression giving access to such module operation. Thus, we can not only automatically instrument our specifications with reusable monitors, but also use them in our specifications and commands as any other module. The rest of the paper is structured as follows. Section 2 presents the rewriting logic language Maude and its Real-Time Maude extension, which allows us to define systems with time annotations. Section 3 presents the structure of monitors we use and basic principles of the approach. Section 4 presents the automatic transformation and the module operation implementing it. Section 5 provides the proof for bisimilarity between the original specification and the instrumented one. Section 6 provides one additional example. Section 7 wraps up the paper with some conclusions and ideas for further extensions and improvements. 2 Maude and Real-Time Maude Maude [2, 3] is an executable formal specification language based on rewriting logic [10], a logic of change that can naturally deal with states and nondeterministic concurrent computations. A rewrite logic theory is a tuple (Σ, E, R), where (Σ, E) is an equational theory that specifies the system states as elements of the initial algebra T(Σ,E), and Ris a set of rewrite rules that describe the one-step possible concurrent transitions in the system. Rewriting operates on congruence classes of terms modulo E. This of course does not mean that an implementation of rewriting logic must have an Ematching algorithm for each equational theory Ethat a user might specify. The equations Eare divided into a set Aof structural axioms for which matching algorithms are available and a set Eof equations. Then, for having a complete agreement between the specification’s initial algebra and its operational semantics by rewriting, a rewrite theory (Σ, E ∪A, R) is assumed to be such that the set Eof equations is (ground) Church-Rosser and terminating modulo A, and the rules Rare (ground) coherent with the equations Emodulo A(see [5, 7]). Maude provides support for rewriting modulo associativity, commutativity and identity, which perfectly captures the evolution of systems made up of objects linked by references. Maude has a rich set of verification and validation tools, and its use is widespread in many fields of research. Furthermore, Maude has demonstrated to be a good environment for rapid prototyping, and also for application development (see [3]). Among the tools and extensions of Maude, one interesting tool for specifying distributed and concurrent systems is Real-Time Maude [14], a rewriting-logicbased specification language and formal analysis tool that supports the formal specification and analysis of real-time systems. Real-Time Maude provides a sort Time to model the time domain, which can be either discrete or dense. Then, passage of time is modelled with tick rules of the form crl [l] : {t,T}=>{t0,T+τ}if C. where tand t0are system states, Tis the global time, and τis a term of sort Time that denotes the duration of the rewrite, and that advances by τthe global time elapse. Since tick rules advance the global time, in Real-Time Maude time elapse is usually modeled by one single tick rule, and the system dynamic behavior by instantaneous transitions [14]. Although there are other sampling strategies, in the most convenient one this single tick rule models time elapse by using two functions: the delta function, that defines the effect of time elapse over every model element, and the mte (maximal time elapse) function, that defines the maximum amount of time that can elapse before any action can be performed. Then, time can advance non-deterministically by any time amount τ, which must be less than or equal to the maximum time elapse of the system. crl [tick] : {t,T}=>{delta(t,τ), T+τ}if 0< τ ≤mte(t)∧C. 3 General monitors In this section we present our proposal for the specification of system-independent monitors. Given a Real-Time Maude object-oriented system specification we provide operations to automatically add objects to measure different properties. We distinguish two types of properties, namely, those on individual objects, e.g., the number of messages received by each node in a network, or the number of defective pieces produced by each machine in a production line, and those on global systems, e.g., the average time taken by messages in reaching their destination or the average failure rate of the machines in a system. We handle both cases uniformly by assuming that there are classes in our specification whose objects “represent” the subsystems being monitored. For instance, we might assume that our network of nodes has a net object with references to all the nodes in it. This would allow us to use an individual monitor associated to the net object instead of a system monitor associated to all the node objects. This might be the case if we wanted to consider, for instance, multiple nets in the same system and separately monitor information on them. We assume a Real-Time Maude object-oriented specification, with a flat configuration of objects and messages (i.e., no nested configurations) and with all rewrite rules of the system defined on terms of sort System, that is, on terms of the form {Conf,T}, with Conf a flat configuration and Ta term of sort Time. To present and illustrate our monitors, we use a very simple specification of a messaging system, shown in Figure 1, where we have interconnected nodes, some of which belong to a subclass a message creator nodes, which create messages to be delivered through the net via specific neighbors. The Node class is defined with an attribute neighbors of type List{Oid}. Its MsgCreator subclass has, in addition, attributes targets, with the identifiers of the nodes it may be addressing messages to, and a counter to limit the number of generated messages. The Net class represents the entire net of nodes. It has an attribute elems with the identifiers of the nodes in the net. Messages are of the form to T via N, without sender identifier nor any contents to simplify the specification, where Tis the identifier of the target node and Nis the neighbor node the message is being sent through. The auxiliary operation pickOne is used to select an element in a list, omod SMP i s pr NAT−TIME−DOMAIN−WITH−INF . i nc R A N D O M +COUNTER . pr L I ST {Oid}. var Msg :Msg .vars O O1 ON :Oid . var VCreator :MsgCreator .var VNode :Nod e . var VNe t :Net .vars T T ’ : TimeInf . vars L L ’EL EL ’ : L ist {Oid}.var N:Nat . var Att s :AttributeSet .var C o n f :Configuration . sort S y s t e m . op {_,_}:C o n f i g u r a t i o n T im e I n f −>S y s t e m [cto r ] . class Net |elems :Lis t {Oid}. class Nod e |neighbors :L i st {Oid}. class MsgCreator |targets :Lis t {Oid },counter :Nat . subclass MsgCreator <Nod e . m sg t o _ v i a _ :Oi d Oid −>Msg . op delay :Ms g Ti m e −>Msg . eq delay(Msg , 0) = Msg . r l [create−msg ] : {<ON :VNet |elems : ( EL O EL ’ ) > <O:VCreator |targets :L,neighbors :L’ , counter :s(N) , At t s >Conf ,T} => {<ON :VNet |elems : ( EL O EL ’ ) > <O:VCreator |targets :L,neighbors :L’ , counter :N,Att s > delay(to pickOne(L,r a n d o m (counter )rem siz e (L) ) via pickOne(L’ , r a n d o m (counter)r em s i z e (L’ ) ) , r a n d o m (counter)rem 500) Conf ,T}. r l [get−msg ] : {<ON :V N et |elems : ( EL O EL ’ ) > <O:VNode |Att s >(to O via O1 )Conf ,T} =>{<ON :VN e t |elems : ( EL O EL ’ ) > <O:VNode |Att s >Conf ,T}. crl [resend−msg ] : {<ON :V Net |elems : ( EL O EL ’ ) > <O:VNode |neighbors :L,Att s > (to O1 via O )Conf ,T} =>{<ON :VN e t |elems : ( EL O EL ’ ) > <O:VNode |neighbors :L,Att s > delay(t o O 1 v ia p i c k O n e (L,r a n d o m (counter)re m si z e (L) ) , r a n d o m (counter)rem 5) Conf ,T} i f O=/= O1 . op pickOne :Lis t {Oid}Nat ˜>Oid . eq pickOne(O L , 0) = O. eq pickOne(O L ,s(N) ) = pickOne(L,N) . op mte :Configuration −>TimeInf . eq mte(delay(Msg ,T)C o nf ) = min(T,mte(C o nf ) ) . eq mte ( ( to O via O1 )Con f ) = 0 . eq mte(Co n f ) = INF [owise ] . op delta :Configuration Time −>Configuration . eq delta(delay(Msg ,T)Conf ,T’ ) =delay(Msg ,T m o n u s T ’ ) delta(Conf ,T’ ) . eq delta(Conf ,T) = C o nf [owise ] . crl [tic k ] : {Conf ,T}=>{delta(Conf ,T’ ) , T+T’} i f T’ := mte (C o nf ) /\0<T’ /\T’<INF . endom Fig. 1. Specification of a simple messaging system omod MONITOR i s pr CONFIGURATION . pr NAT−TIME−DOMAIN−WITH−INF . sort Dat a . class @Monitor |o:Object ,dat a :D a ta . op eva l :Data Time Object Configuration Configuration Configuration −>Da t a . op mon :Oid −>Oid [ct o r ] . endom Fig. 2. Core of monitors which will be used in the create-msg and resend-msg rules to randomly select elements in the list of targets and neighbors. The create-msg rule creates a new message addressed to a random target via a random neighbor, the get-msg specifies the reception of a message by its addressee, and the resend-msg rule specifies the action in which a node receives a message that is not addressed for it and resends it via one of its neighbors. Note that such rule will resend the message via one of its randomly chosen neighbors. Delays in message delivery is specified with the usual delay operator (see [14]). Real-Time Maude’s tick rule and mte and delta functions are defined as usual. Inspired by the works on wrapper objects, and specifically on the Onion-Skin pattern [13, 11], we add monitors to our specification by means of wrappers. We will show a generic monitor structure that, by specifying the definition of the data structure and the query for the monitor to use, can be instantiated to a concrete monitor to be added to our system. Each object to be monitored is wrapped inside a monitor object that will observe its behavior and will collect the required information on it. This generic monitor structure is defined by the MONITOR module in Figure 2. There is a class @Monitor whose instances will wrap objects in their oattributes. The data of the monitor is stored in the attribute data, of sort Data, to be later instantiated depending on the specific kind of monitor defined. There is an operation eval, that will be used to recalculate the monitored information, depending on the actions specified in individual rules, with parameters: (i) the current monitor’s data, (ii) the time at which the expression is evaluated, (iii) the monitored object in the LHS of the rule, (iv) the objects and messages explicitly stated in the rule’s LHS, (v) the objects and messages in the rule’s RHS, and (vi) the rest of the LHS’ configuration. The individual monitor of an object with identifier Owill have identifier mon(O). Specific monitors can be defined by specifying of the function eval, which could be defined over any data structure, just by appropriately subsorting the sort Data. For example, given the simple messaging system specified in the module in Figure 1, we may count the number of messages received by each of the nodes in the system by wrapping each of them inside monitor objects as in Figure 4, and by defining the eval function in a module TRAFFIC-MONITOR extending the MONITOR module, given an auxiliary #msgs function which counts the number of messages in a configuration, as shown in Figure 3. Note that the data attribute remains unchanged in the create-msg rule, but it is recalculated in rules get-msg and resend-msg, those rules in which node objects receive messages. omod TRAFFIC−MONITOR i s i nc M O N I T O R . pr NAT . subsort Nat <Dat a . var N:Nat . var T:Tim e . var Obj :O b j e c t . vars LConf RConf GConf :Configuration . eq eval (N,T,Obj ,LConf ,RC onf ,GConf) =N+ #ms g s (LConf) . op #ms g s :Configuration −>Nat . eq #msg s (Msg C onf ) = s(#m sgs (C o n f ) ) . eq #msg s (C o nf ) = 0 [ owise ] . endom Fig. 3. Traffic monitors The subsort relation states the data type of the monitor data. This monitor is going to store only a natural number, used to count the number of messages the node at hand has processed. Note that the operation eval is total and it will increment the natural number stored in the monitor with the number of messages in the rule’s LHS. By rewriting our initial configuration with our nodes wrapped inside monitor objects using the rules in Figure 4, we get a final configuration in which the data attributes of each of the monitor objects contains the number of messages received by that node. 4 Construction of the instrumented specification The construction of instrumented specifications has been automated by providing a module expression MONITOR that takes as arguments the specification to be monitored, the class whose objects are to be wrapped, the set of rules on which the measures are to be evaluated, and a concrete monitor to apply to it, in which the Data sort and the eval functions are defined, and that produces the corresponding new module. The module expression is integrated in Full Maude and is handled as any other module expression [6]. Given an object-oriented system specification S, a class C, a set of rule labels LS, and a concrete monitor M, the rewrite theory M[S, C, LS, E] denotes the system Sbut now instrumented with the monitor Eas follows: –M[S, C, LS, E] includes both Sand M, plus transformed copies of the rules of Sso that each rule of the form var Msg :Msg .vars O O1 ON :Oid . var VCreator :MsgCreator .var VNode :Nod e . vars L L ’EL EL ’ : L ist {Oid}.var N:Nat . vars Att s @ A t t s :AttributeSet .var C onf :Configuration . vars T T ’ : TimeInf .var V Net :Net . var @D :Data . r l [create−msg ] : {<ON :VNet |elems : ( EL O EL ’ ) > <mon(O) : @Monitor | o:<O:VCreator | targets :L,neighbors :L’ , counter :s(N)> > Con f ,T} => {<ON :VNet |elems : ( EL O EL ’ ) > <mon(O) : @Monitor | o:<O:VCreator | targets :L,neighbors :L’ , counter :N> > delay(to pickOne(L,r a n d o m (counter )rem siz e (L) ) via pickOne(L’ , r a n d o m (counter)r em s i z e (L’ ) ) , r a n d o m (counter)rem 500) Con f ,T}. r l [get−msg ] : {<ON :V N et |elems : ( EL O EL ’ ) > <mon(O) : @Monitor |o:<O:VNode |Att s > > (to O via O1 )Conf ,T} =>{<ON :VN e t |elems : ( EL O EL ’ ) > <mon(O) : @Monitor |o:<O:VNode |Att s > > Conf ,T}. crl [resend−msg ] : {<ON :V Net |elems : ( EL O EL ’ ) > <mon(O) : @Monitor | o:<O:VNode |neighbors :L>, dat a :@D > (to O1 via O )Conf ,T} =>{<ON :VN e t |elems : ( EL O EL ’ ) > <mon(O) : @Monitor | o:<O:VNode |neighbors :L>, dat a :e v al (@D ,T, <O:VNode |neighbors :L>, (<ON :VNet |elems : ( EL O EL ’ ) > <O:VNode |neighbors :L>(to O1 via O ) ) , (<ON :VNet |elems : ( EL O EL ’ ) > <O:VNode |neighbors :L> delay(to O1 v ia p i c k O n e (L,r a n d o m (counter)re m si z e (L) ) , r a n d o m (counter)rem 5) ) , Con f )> delay(t o O 1 v ia p i c k O n e (L,r a n d o m (counter)re m si z e (L) ) , r a n d o m (counter)rem 5) Conf ,T} i f O=/= O1 . Fig. 4. Rules of the simple messaging system with individual monitors crl [L] : {< O :C0|Atts >Conf ,T} =>{< O :C0|Atts0>Conf 0,T} i f Cond . with C0a subclass of Cor Citself, and Lin LS, generates a new rule crl [L] : {<mon(O) : Monitor |o:< O :C|Atts >,d ata :D > Conf ,T} => {<mon(O) : Monitor | o:< O :C|Atts0>, dat a :e v al (D,T, < O :C|Atts >, Conf , < O :C|Atts0>Conf 0)> Conf 0, T} i f Cond . –All other occurrences of objects < O :C|Atts > of subclasses of Cin rules, equations and memberships will be rewritten as <mon(O) : Monitor |o:< O :C|Atts >,d ata :D >. –All other objects in rules are left as they were. –In case multiple objects appear in the same rule/equation/membership, different Dvariables will be consistently used. E.g., if Lis not in LS, for a rule with two objects of class Cin its left-hand side, the following rule will be generated: crl [L] : {<mon(O1) : Monitor |o:< O1 : C|Atts1 >,da t a :D1> <mon(O2) : Monitor |o:< O2 : C|Atts2 >,da t a :D2> Conf ,T} => {<mon(O1) : Monitor |o:< O1 : C|Atts10>,da t a :D1> <mon(O2) : Monitor |o:< O2 : C|Atts20>,da t a :D2> Conf 0,T} Note that: –Those rules with no objects in subclasses of Cremain as in the original module, and –There might be more than one object in subclasses of Cin the lefthand side of a rule, in which case the above transformation has to be applied to each of them, that is, we must consider all possible matches of the above pattern. E.g., given a rule crl [L] : {< O1 : C1|Atts1 > < O2 : C2|Atts2 > Conf ,T} => {< O1 : C1|Atts10> < O2 : C2|Atts20> Conf 0,T} i f Cond . 5. F. Dur´an, S. Lucas, C. March´e, J. Meseguer, and X. Urbain. Proving operational termination of membership equational programs. Higher-Order and Symbolic Computation, 21(1-2):59–88, 2008. 6. F. Dur´an and J. Meseguer. Maude’s module algebra. Science of Computer Programming, 66(2):125–153, April 2007. 7. F. Dur´an and J. Meseguer. On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories. J. Log. Algebr. Program., 81(7-8):816– 850, 2012. 8. G. J. Holzmann. The SPIN Model Checker. Addison-Wesley, 2003. 9. I. Lee, S. Kannan, M. Kim, O. Sokolsky, and M. Viswanathan. Runtime assurance based on formal specifications. In H. R. Arabnia, editor, Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, PDPTA 1999, June 28 - Junlly 1, 1999, Las Vegas, Nevada, USA, pages 279–287. CSREA Press, 1999. 10. J. Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science, 96(1):73–155, 1992. 11. J. Meseguer. Taming distributed system complexity through formal patterns. Sci. Comput. Program., 83:3–34, 2014. 12. J. Meseguer, M. Palomino, and N. Mart´ı-Oliet. Algebraic simulations. J. Log. Algebr. Program., 79(2):103–143, 2010. 13. J. Meseguer and C. L. Talcott. Semantic models for distributed object reflection. In B. Magnusson, editor, ECOOP 2002 - Object-Oriented Programming, 16th European Conference, Malaga, Spain, June 10-14, 2002, Proceedings, volume 2374 of Lecture Notes in Computer Science, pages 1–36. Springer, 2002. 14. P. C. ¨ Olveczky and J. Meseguer. Semantics and pragmatics of Real-Time Maude. Higher-Order and Symbolic Computation, 20(1-2):161–196, 2007. 15. C. Rocha and J. Meseguer. Proving safety properties of rewrite theories. In A. Corradini, B. Klin, and C. Cˆırstea, editors, Algebra and Coalgebra in Computer Science - 4th International Conference, CALCO 2011, Winchester, UK, August 30 - September 2, 2011. Proceedings, volume 6859 of Lecture Notes in Computer Science, pages 314–328. Springer, 2011. 16. J. Troya, A. Vallecillo, F. Dur´an, and S. Zschaler. Model-driven performance analysis of rule-based domain specific visual models. Information & Software Technology, 55(1):88–110, 2013. 17. S. Zschaler. Formal specification of non-functional properties of component-based software systems. Software and System Modeling, 9(2):161–201, 2010.