E-Book, Englisch, Band 157, 339 Seiten, eBook
Reihe: IFIP International Federation for Information Processing
Reis Information Technology
1. Auflage 2006
ISBN: 978-1-4020-8159-0
Verlag: Springer US
Format: PDF
Kopierschutz: 1 - PDF Watermark
Selected Tutorials
E-Book, Englisch, Band 157, 339 Seiten, eBook
Reihe: IFIP International Federation for Information Processing
ISBN: 978-1-4020-8159-0
Verlag: Springer US
Format: PDF
Kopierschutz: 1 - PDF Watermark
Zielgruppe
Research
Autoren/Hrsg.
Weitere Infos & Material
Quality of Service in Information Networks.- Risk-Driven Development of Security-Critical Systems Using UMLsec.- Developing Portable Software.- Formal Reasoning About Systems, Software and Hardware.- The Problematic of Distributed Systems Supervision - An Example: GeneSyS.- Software Rejuvenation - Modeling and Analysis.- Test and Design-for-Test of Mixed-Signal Integrated Circuits.- Web Services.- Applications of Multi-Agent Systems.- Discrete Event Simulation with Application to Computer Communication Systems Performance.- Human-Centered Automation: A Matter of Agent Design and Cognitive Function Allocation.
5. Security evaluation of UML diagrams using formal semantics (p. 26- 27)
For some of the constraints used to define the UMLsec extensions we need to refer to a precisely defined semantics of behavioral aspects, because verifying whether they hold for a given UML model may be mathematically non-trivial. Firstly, the semantics is used to define these constraints in a mathematically precise way. Secondly, in ongoing work, we are developing mechanical tool support for analyzing UML specifications (for example in [Sha03; Men], and a few other student projects). For this, a precise definition of the meaning of the specifications is necessary, and it is useful to formulate this as a formal model for future reference before coding it up. For security analysis, the security-relevant information from the security-oriented stereotypes is then incorporated.
Note that because of the complexities of the UML, it would take up too much space to recall our formal semantics here completely. Instead, we just define precisely and explain the interfaces of the semantics that we need here to define the UMLsec profile. More details on the formal semantics can be found in [Jür03b]. Our formal semantics of a simplified fragment of UML using Abstract State Machines (ASMs) includes the following kinds of diagrams:
Class diagrams define the static class structure of the system: classes with attributes, operations, and signals and relationships between classes.
On the instance level, the corresponding diagrams are called object diagrams.
Statechart diagrams (or state diagrams) give the dynamic behavior of an individual object or component: events may cause a change in state or an execution of actions.
Sequence diagrams describe interaction between objects or system components via message exchange.
Activity diagrams specify the control flow between several components within the system, usually at a higher degree of abstraction than statecharts and sequence diagrams. They can be used to put objects or components in the context of overall system behavior or to explain use cases in more detail.
Deployment diagrams describe the physical layer on which the system is to be implemented.
Subsystems (a certain kind of packages) integrate the information between the different kinds of diagrams and between different parts of the system specification.
There is another kind of diagrams, the use case diagrams, which describe typical interactions between a user and a computer system. They are often used in an informal way for negotiation with a customer before a system is designed. We will not use it in the following. Additionally to sequence diagrams, there are collaboration diagrams, which present similar information. Also, there are component diagrams, presenting part of the information contained in deployment diagrams.
The used fragment of UML is simplified significantly to keep a formal treatment that is necessary for some of the more subtle security requirements feasible and to allow model-checking of UML specifications. Note also that in our approach we identify system objects with UML objects, which is suitable for our purposes. Also, as with practical all analysis methods, also in the real-time setting [Wat02], we are mainly concerned with instance-based models.
Although simplified, our choice of a subset of UML is reasonable for our needs, as we have demonstrated in several industrial case-studies (some of which are documented in [Jür03b]).