Browsing by Author "Prashanth, C.M."
Now showing 1 - 6 of 6
- Results Per Page
- Sort Options
Item An efficient event based approach for verification of UML statechart model for reactive Systems(2008) Prashanth, C.M.; Shet, K.C.; Elamkulam, J.Abstract-This paper describes an efficient method to detect safety specification violations in dynamic behavior model of concurrent/reactive systems. The dynamic behavior of each concurrent object in a reactive system is assumed to be represented using UML (Unified Modeling Language) statechart diagram. The verification process involves building a global state space graph from these independent statechart diagrams and traversal of large number of states in global state space graph for detecting a safety violation. In our approach, a safety property to be verified is read first and a set of events, which could violate this property, is computed from the model description. We call them as "relevant events". The global state space graph is constructed considering only state transitions caused by the occurrence of these relevant events. This method reduces the number of states to be traversed for finding a property violation. Hence, this technique scales well for complex reactive systems. As a case study, the proposed technique is applied to verification of Generalized Railroad Crossing (GRC) system and safety property "When train is at railroad crossing, the gate always remain closed" is checked. We could detect a flaw in the infant UML model and eventually, correct model is built with the help of counter example generated. The result of the study shows that, this technique reduces search space by 59% for the GRC example. © 2008 IEEE.Item Efficient algorithms for verification of UML statechart models(Academy Publisher, 2009) Prashanth, C.M.; Shet, K.C.In this article, we present algorithms devised for the automatic verification of UML(Unified Modeling Language) statechart models. The basic algorithm checks the safety property violation during the construction (on-the-fly) of the state space graph and if any property violation is found, it generates a counter example. The second algorithm builds the state space considering only those events, which could lead to the negative behavior of the system. In other words, a set of relevant events is generated first and state space is constructed considering only the state transitions of the objects caused by these relevant events. Thus search space is reduced in both the methods. As a case study, we have verified UML statechart model of the Generalized Railroad Crossing (GRC) system using the proposed algorithms. The safety property When the train is at rail road crossing, the gate always remain closed is verified. We could detect property violation in the initial UML statechart model of GRC and eventually it is corrected with the help of the counter example generated by the algorithms. The case study results show that event based verification algorithm yields 59% reduction in the state space for the GRC example. © 2009 ACADEMY PUBLISHER.Item An efficient event based approach for verification of UML statechart model for reactive Systems(2008) Prashanth, C.M.; Shet, K.C.; Elamkulam, J.Abstract-This paper describes an efficient method to detect safety specification violations in dynamic behavior model of concurrent/reactive systems. The dynamic behavior of each concurrent object in a reactive system is assumed to be represented using UML (Unified Modeling Language) statechart diagram. The verification process involves building a global state space graph from these independent statechart diagrams and traversal of large number of states in global state space graph for detecting a safety violation. In our approach, a safety property to be verified is read first and a set of events, which could violate this property, is computed from the model description. We call them as "relevant events". The global state space graph is constructed considering only state transitions caused by the occurrence of these relevant events. This method reduces the number of states to be traversed for finding a property violation. Hence, this technique scales well for complex reactive systems. As a case study, the proposed technique is applied to verification of Generalized Railroad Crossing (GRC) system and safety property "When train is at railroad crossing, the gate always remain closed" is checked. We could detect a flaw in the infant UML model and eventually, correct model is built with the help of counter example generated. The result of the study shows that, this technique reduces search space by 59% for the GRC example. � 2008 IEEE.Item Verification framework for detecting safety violations in UML statecharts(2008) Prashanth, C.M.; Shet, K.C.; Elamkulam, J.The model based development is a widely accepted phenomenon to build dependable software. This has lead to development of tools which can generate deployable code from the model. Hence, ensuring the correctness of such models becomes extremely important. Model checking technique can be applied to detect specification violations in such models at the early stage of development life cycle. In practice, such validations are done using off-the-shelf model checkers. This technique though popular has a drawback that, model should be described in the native language of the model checker. In this paper, we propose a framework for the verification of the dynamic behavior of reactive systems modeled using UML (Unified Modeling Language) statechart diagrams. The model is translated to an intermediate representation by parsing the information embedded behind the UML Statecharts, this intermediate representation is used for checking the safety violations. Verification framework proposed is scalable to complex systems. � 2008 IEEE.Item Verification framework for detecting safety violations in UML statecharts(2008) Prashanth, C.M.; Shet, K.C.; Elamkulam, J.The model based development is a widely accepted phenomenon to build dependable software. This has lead to development of tools which can generate deployable code from the model. Hence, ensuring the correctness of such models becomes extremely important. Model checking technique can be applied to detect specification violations in such models at the early stage of development life cycle. In practice, such validations are done using off-the-shelf model checkers. This technique though popular has a drawback that, model should be described in the native language of the model checker. In this paper, we propose a framework for the verification of the dynamic behavior of reactive systems modeled using UML (Unified Modeling Language) statechart diagrams. The model is translated to an intermediate representation by parsing the information embedded behind the UML Statecharts, this intermediate representation is used for checking the safety violations. Verification framework proposed is scalable to complex systems. © 2008 IEEE.Item Verification of protocol design using UML - SMV(2009) Prashanth, C.M.; Chandrashekar Shet, K.In recent past, the Unified Modeling Language (UML) has become the de facto industry standard for object-oriented modeling of the software systems. The syntax and semantics rich UML has encouraged industry to develop several supporting tools including those capable of generating deployable product (code) from the UML models. As a consequence, ensuring the correctness of the model/design has become challenging and extremely important task. In this paper, we present an approach for automatic verification of protocol model/design. As a case study, Session Initiation Protocol (SIP) design is verified for the property, "the CALLER will not converse with the CALLEE before the connection is established between them ". The SIP is modeled using UML statechart diagrams and the desired properties are expressed in temporal logic. Our prototype verifier "UML-SMV" is used to carry out the verification. We subjected an erroneous SIP model to the UML-SMV, the verifier could successfully detect the error (in 76.26ms) and generate the error trace.