Fragmente (Plagiat, gesichtet)
Kein Fragment
Fragmente (Plagiat, ungesichtet)
5 Fragmente
| [1.] Analyse:Sad/Fragment 051 07 - Diskussion Bearbeitet: 14. March 2018, 19:45 Graf Isolan Erstellt: 14. March 2018, 19:42 (Graf Isolan) | BauernOpfer, Fragment, SMWFragment, Sad, Schutzlevel, Schäfer et al 2001, ZuSichten |
|
|
|
| Untersuchte Arbeit: Seite: 51, Zeilen: 7-11 |
Quelle: Schäfer et al 2001 Seite(n): 1, Zeilen: 9ff. |
|---|---|
| The Unified Modeling Language provides two complementary notations, state machines and collaborations, for the specification of dynamic system behavior. HUGO is designed to automatically verify whether the interactions expressed by a collaboration can indeed be realized by a set of state machines [SKM01]. HUGO compile state machines into a PROMELA model and collaborations into set of Büchi automata (”never claims”).
[SKM01] Tim Schaefer, Alexander Knapp, and Stephan. Merz. Model checking uml state machines and collaborations. In Scott D. Stoller and Willem Visser, editors, Proc. Wsh. Software Model Checking, volume 55(3) of Electr. Notes Theo. Comp. Sci., 2001. 13 pages. |
Abstract
The Unified Modeling Language provides two complementary notations, state machines and collaborations, for the specification of dynamic system behavior. We describe a prototype tool, HUGO, that is designed to automatically verify whether the interactions expressed by a collaboration can indeed be realized by a set of state machines. We compile state machines into a PROMELA model and collaborations into sets of Büchi automata (“never claims”). |
Although identical nothing has been marked as a citation. The source is given in passing. |
|
| [2.] Analyse:Sad/Fragment 057 17 - Diskussion Bearbeitet: 14. March 2018, 20:12 Graf Isolan Erstellt: 14. March 2018, 20:00 (Graf Isolan) | Fragment, KomplettPlagiat, SMWFragment, Sad, Schutzlevel, Schäfer et al 2001, ZuSichten |
|
|
|
| Untersuchte Arbeit: Seite: 57, Zeilen: (16), 17-30 |
Quelle: Schäfer et al 2001 Seite(n): 1-2, Zeilen: 1:30-33-2:1-10.18-21 |
|---|---|
| 2.4.2 HUGO Model Checker
HUGO is a prototype tool designed to automatically verify whether the interactions expressed by a collaboration diagram can indeed be realized by a set of state machines. Technically, this is achieved by compiling state machines into a PROMELA model, and collaborations into sets of BÜchi automata 2 (” never claim”). The model checker SPIN is then called to verify the model against the automata. The idea to analyze UML state machines and other variants of Statecharts using model checking has been suggested before [Kwo00,LMM99,LP99, MLS97, MLSH99], but HUGO is based on dynamic computation of Statechart behavior rather than a pre-determined, static calculation of possible state transitions in response to input events. HUGO has the advantage of being more modular, more flexible, and easier to adapt to variants of Statechart semantics, including possible changes to the semantics of UML state machines. Besides model checking, HUGO also supports animation and the generation of Java code from UML state machine models, based on the same structure of implementation. HUGO provides us also the correctness of the generated code with respect to the properties verified from the PROMELA model. (see figure 2.11) 2 A Büchi automata is the extension of a finite state machine to infinite inputs. It accepts an infinite input sequence, iff there exists a run of the automaton (in case of a deterministic automaton, there is exactly one possible run) which has infinitely many states in the set of final states. It is named after the Swiss mathematician Julius Richard Büchi. Finite state machine (FSM) is a model of behavior composed of a finite number of states, transitions between those states, and actions. [Kwo00] G. Kwon. Rewrite rules and operational semantics for model checking uml statecharts. In : A. Evans, S. Kent and B. Selic, editors, Proc. 3nd Int. Conf. UML, Lect. Notes Comp. Sci. 1939, pages 528–440, 2000. [LMM99] D. Latella, I. Majzik, and M. Massink. Automatic verification of a behavioural subset of uml statechart diagrams using the spin model-checker. In Formal Aspects Comp. 11, pages 637–664, 1999. [LP99] J. Lilius and I. P. Paltor. Formalising uml state machines for model checking. In : R. B. France and B. Rumpe, editors, Proc. 2nd Int. Conf. UML, Lect. Notes Comp. Sci. 1723, pages 430–445, 1999. [MLS97] E. Mikk, Y. Lakhnech, and M. Siegel. Hierarchical automata as model for statecharts. In : R. K. Shyamasundar and K. Ueda, editors, Proc. 3nd Asian Computing Science Conf., Lect. Notes Comp. Sci. 1345, pages 181–196, 1997. [MLSH99] E. Mikk, Y. Lakhnech, M. Siegel, and G.J. Holzmann. Implementing statecharts in promela/spin. In Proc. Wsh. Industrial-Strength Formal Specification Techniques, 1999. |
[page 1]
In this paper we describe HUGO, a prototype tool designed to automatically verify whether the interactions expressed by a collaboration diagram can indeed be realized by a set of state machines. Technically, this is achieved by compiling state machines into a PROMELA [1] model, and collaborations into sets of Büchi [page 2] automata (“never claims”). The model checker SPIN is then called upon to verify the model against the automata. The idea to analyze UML state machines and other variants of Statecharts using model checking has been suggested before [2,3,4,5,6], although we are not aware of other tools that verify state machines against collaboration diagrams. In contrast to most other encodings of Statecharts, ours is based on a dynamic computation of Statechart behavior rather than a pre-determined, static calculation of possible state transitions in response to input events. Our approach has the advantage of being more modular, more flexible, and easier to adapt to variants of Statechart semantics, including possible changes to the semantics of UML state machines. [...] Besides model checking, HUGO also supports animation and the generation of Java code from UML state machine models, based on the same structure of implementation. Our aim is to ensure the correctness of the generated code with respect to the properties verified from the PROMELA model. [1] Holzmann, G. J., The SPIN Model Checker, IEEE Trans. Softw. Eng. 23 (1997), pp. 279–295. [2] Kwon, G., Rewrite Rules and Operational Semantics for Model Checking UML Statecharts, in: A. Evans, S. Kent and B. Selic, editors, Proc. 3nd Int. Conf. UML, Lect. Notes Comp. Sci. 1939 (2000), pp. 528–540. [3] Latella, D., I. Majzik and M. Massink, Automatic Verification of a Behavioural Subset of UML Statechart Diagrams Using the SPIN Model-Checker, Formal Aspects Comp. 11 (1999), pp. 637–664. [4] Lilius, J. and I. P. Paltor, Formalising UML State Machines for Model Checking, in: R. B. France and B. Rumpe, editors, Proc. 2nd Int. Conf. UML, Lect. Notes Comp. Sci. 1723 (1999), pp. 430–445. [5] Mikk, E., Y. Lakhnech and M. Siegel, Hierarchical Automata as Model for Statecharts, in: R. K. Shyamasundar and K. Ueda, editors, Proc. 3rd Asian Computing Science Conf., Lect. Notes Comp. Sci. 1345 (1997), pp. 181–196. [6] Mikk, E., Y. Lakhnech, M. Siegel and G. J. Holzmann, Implementing Statecharts in Promela/SPIN, in: Proc. IEEE Wsh. Industrial-Strength Formal Specification Techniques (1999). |
Although identical - including references - nothing has been marked as a citation. the original source is not given here. |
|
| [3.] Analyse:Sad/Fragment 059 11 - Diskussion Bearbeitet: 12. March 2018, 20:56 Graf Isolan Erstellt: 12. March 2018, 20:45 (Graf Isolan) | Fragment, KomplettPlagiat, SMWFragment, Sad, Schutzlevel, Schäfer et al 2001, ZuSichten |
|
|
|
| Untersuchte Arbeit: Seite: 59, Zeilen: 11-18 |
Quelle: Schäfer et al 2001 Seite(n): 4, Zeilen: 30-32, 33ff. |
|---|---|
| This example of ATM simulate the interaction of an ATM with a single hypothetical user and a bank computer. The simulation focuses on card and PIN validation, after the user has entered his bank card, the ATM requests a PIN to be entered and then asks the bank to verify the entry, waiting for a reply. If both card and PIN are valid, the ATM may proceed to dispense money; if the PIN is invalid the ATM will have the user reenter the PIN; if the card is invalid the ATM will be requested to abort the transaction and return the card immediately (this ATM does not keep invalid cards). After having retrieved his card, the user may reenter the same card as many times as he wishes or end [the interaction.] | The example state machines simulate the interaction of an ATM with a single hypothetical user and a bank computer. The simulation focuses on card and PIN validation and we abstract from all other interactions by using completion transitions on most of the states, serving to sustain the progress of the simulation. After the user has entered his bank card, the ATM requests a PIN to be entered and then asks the bank to verify the entry, waiting for a reply. If both card and PIN are valid, the ATM may proceed to dispense money; if the PIN is invalid the ATM will have the user reenter the PIN; if the card is invalid the ATM will be requested to abort the transaction and return the card immediately (this ATM does not keep invalid cards). After having retrieved his card, the user may reenter the same card as many times as he wishes or end the interaction. |
Although identical nothing has been marked as a citation. The source is given at the end of the first paragraph on the page following. |
|
| [4.] Analyse:Sad/Fragment 060 01 - Diskussion Bearbeitet: 13. March 2018, 09:44 Graf Isolan Erstellt: 13. March 2018, 09:39 (Graf Isolan) | BauernOpfer, Fragment, SMWFragment, Sad, Schutzlevel, Schäfer et al 2001, ZuSichten |
|
|
|
| Untersuchte Arbeit: Seite: 60, Zeilen: 1-9 |
Quelle: Schäfer et al 2001 Seite(n): 4-5, Zeilen: 4:40ff. - 5:1-5 |
|---|---|
| Figure 2.14: State Machine of the atm in ATM
As shown in Fig. 2.13, the bank computer validates the bank card concurrently to the PIN code. If the card is not valid, the concurrent validation is exited immediately and the ATM is requested to abort the transaction. The completion transition leaving VerifyingPIN simulates any possible PIN entry by branching non-deterministically into the states PINCorrect and PINIncorrect. The two join transitions evaluate the results of the concurrent validations. If an incorrect PIN has been entered and the card is valid, the counter of invalid PIN entries is incremented; however, if the counter numIncorrect exceeded a maximum value, the card is invalidated and the transaction aborted. In contrast, if a correct PIN has been entered, the counter is reset to zero [SKM01]. [SKM01] Tim Schaefer, Alexander Knapp, and Stephan. Merz. Model checking uml state machines and collaborations. In Scott D. Stoller and Willem Visser, editors, Proc. Wsh. Software Model Checking, volume 55(3) of Electr. Notes Theo. Comp. Sci., 2001. 13 pages. |
[page 4]
As shown in fig. 1(e), the bank computer validates the bank card concurrently to the PIN code. If the card is not valid, the concurrent validation is exited immediately and the ATM is requested to abort the transaction. The completion transition leaving VerifyingPIN simulates any possible PIN entry by branching non-deterministically into the states PINCorrect and PIN- [page 5] Incorrect. The two join transitions evaluate the results of the concurrent validations. If an incorrect PIN has been entered and the card is valid, the counter of invalid PIN entries is incremented; however, if the counter has exceeded a maximum value, the card is invalidated and the transaction aborted. In contrast, if a correct PIN has been entered, the counter is reset to zero. [page 7] (d) State machine diagram for class ATM Fig. 1. UML model of an ATM |
Identical with no part of it being marked as a citation. The source is named in passing at the end of the paragraph. The figures also show identical state machine diagrams (though drawn slightly different). |
|
| [5.] Analyse:Sad/Fragment 060 10 - Diskussion Bearbeitet: 13. March 2018, 09:49 Graf Isolan Erstellt: 13. March 2018, 09:49 (Graf Isolan) | BauernOpfer, Fragment, SMWFragment, Sad, Schutzlevel, Schäfer et al 2001, ZuSichten |
|
|
|
| Untersuchte Arbeit: Seite: 60, Zeilen: 10-14 |
Quelle: Schäfer et al 2001 Seite(n): 9, Zeilen: 32-38 |
|---|---|
| Verifying Collaborations HUGO is mainly intended to verify whether certain specified collaborations are indeed feasible for the required state machines. To do so, it generates B¨uchi automata that accept all executions that conform to the collaboration, and calls on SPIN to verify that no execution of the model is accepted by these ”never claims”. If the collaboration is possible, SPIN will produce a ”counter example” that allows the successful execution to be replayed. | 4 Verifying Collaborations
HUGO is mainly intended to verify whether certain specified collaborations are indeed feasible for a set of UML state machines. To do so, it generates B¨uchi automata that accept all executions that conform to the collaboration, and calls on SPIN to verify that no execution of the model is accepted by these “never claims”. If the collaboration is possible, SPIN will produce a “counter example” that allows the successful execution to be replayed. |
Identical with no part of it being marked as a citation. It is by far not clear that the reference given by SAD at the end of the previous paragraph should be thought to extend to this paragraph also. |
|
Fragmente (Verdächtig / Keine Wertung)
Kein Fragment
Fragmente (Kein Plagiat)
Kein Fragment
Fragmente (Verwaist)
Kein Fragment
Quellen
| Quelle | Autor | Titel | Verlag | Jahr | Lit.-V. | FN |
|---|---|---|---|---|---|---|
| Sad/Schäfer et al 2001 | Timm Schäfer and Alexander Knapp and Stephan Merz | Model Checking UML State Machines and Collaborations | 2001 | no | yes |
Übersicht
| Typus | Gesichtet | ZuSichten | Unfertig | Σ |
|---|---|---|---|---|
| KP | 0 | 2 | 0 | 2 |
| VS | 0 | 0 | 0 | 0 |
| ÜP | 0 | 0 | 0 | 0 |
| BO | 0 | 3 | 0 | 3 |
| KW | 0 | 0 | 0 | 0 |
| KeinP | 0 | 0 | 0 | 0 |
| Σ | 0 | 5 | 0 | 5 |
Sitemap
Wichtige Seiten
Befunde
Alle Fragmente