|
Modeling and Evaluation of Dependable Systems1. Quantitative Analysis of UML-Statecharts by simulation. The evaluation of systems concerning issues of fault tolerance and
reliability becomes nowadays, due to increasingly use of embedded
systems, more important. Of particular importance is to analyze and
evaluate the system, based on the system model, on early stages of the
modeling process. The starting point thereby are UML models
(UML-Statecharts). UML was established in the last years as the
De-Facto-standard of the industry and meanwhile the version 2.0 is about
to be released.
The complete transformation of the UML-statecharts in Stochastic Reward
Nets allows the modeler to evaluate its models both analytically and
simulative. It was particularly important to consider all the model
elements of the UML-Statecharts and not only to transform a limited set
of the UML concepts. The modeler does not have to do without certain
concepts, which possibly could not be mapped into Stochastic Reward
nets.
The biggest challenge of the transformation was to transform the
UML-Statecharts, with step semantics, to an equivalent Stochastic Reward
Net, with interleaving semantics. In a UML-Statechart several
transitions can fire at time (in the same step). In a Petri Net only one
transition can fire at time, even if several transitions are activated
and could fire. As a result of the different semantics (step versus
interleaving) the Petri Net can reach a configuration, which is not
possible in the UML-Statechart. In order to avoid this problem, all the
transitions of the statechart, which can fire at the same time, had to
be merged into a single transition in the Petri Net, i.e. the same event
triggers several transitions.
This problem does not occur, with Complition transitions - transitions
that are triggered without an event and are able to fire as soon as the
source state of the transition is entered and all possibly occurring
entry and exit events are generated - since according to UML standard
all the complition transitions fire successively, which is equivalent to
the Interleaving semantics of the Petri Net.
In addition event handling was defined. This step was necessary, since
in the UML standard nothing is stated over the order of the generation
and treatment of events. The transformer generates the appropriate
Stochastic Reward Net from the model, which is provided and stored in
the XMI format. The UML models can be provided thereby by different CASE
Tools. Currently models generated by Poseidon/Gentleware, Innovator/MID,
Rational Rose/IBM are supported. Other Tools can be considered as soon
as they provide an XML export of the system model.
The simulator simulates the Stochastic Reward Net and thus also the
complete statechart model. From the simulation the appropriate
information about the system can be derived.
An analytic evaluation of the model is possible under the condition,
that the state space does not explode, which in particular can occur
when complex models are considered. In order to deal with this problem a
simplification of the system model, which leads usually to trivial
models, could help. Therefore the simulative evaluation of the complete
model is to be preferred in such cases. (K. Kosmidis) 2. Patterns and Scenarios in UML The development of a semantically founded representation of patterns
and scenarios by means of the UML and of procedures for the verification
of implementations against such specifications was continued.
For the representation both of requirements of the implementation of a
system and of patterns which are to play a role in the context of the
implementation, the collaboration seems to be the element particularly
suituable from the repertoire of the UML. A Collaboration is
a set of related objects, regarded to the respect of some concrete roles.
They form a scenario, i.e. exchange a sequence of messages to meet
a certain goal. For the representation of the implementaion of the
system is primarily accomplished by using class diagrams for the static
structure, as well as state chart diagrams for the description of behavior.
Between the system's complete behavioral specification on the one hand
and scenarios on the other, a cross-check is to be realized, which examines
them for consistency. To this end it is absolutely necessary to formally
specify the semantics of all required parts of the UML in an appropriate way.
On closer examination of the methodical aspects of analysis and design of
complex interacting systems it showed up that it is useful to sketch out a
UML-profile which facilitates the binding and embedding of patterns and
scenarios to models for the user. By defining suitable restrictions to
syntax and semantics and not least documentation it offers the modeler an
orientational guideline for the deployment of patterns. The detailed
development of such a profile forms one of the principal objectives of
the work for the near future.
(M. Sand) 3. Specification of Systems and Components using Formal and Semiformal Methods The project's objective was the analysis in how far ASIC design processes at Lucent Technologies
can be supported by the introduction of formal methods.
The traditional verification tasks at Lucent were analyzed,
the used test methods and cases were classified
and a table based-specification method (Advanced Design and Verification of ASICS - ADeVA)
was developed. (S. Gossens) | Project manager: Prof. a.D. Dr. Dr. h.c. Mario Dal Cin
Project participants: Dipl.-Inf. Stefan Gossens, Dipl.-Inf. Konstantinos Kosmidis, Dipl.-Inf. David Kreische, Dr.-Ing. Matthias Sand, F. Wang
Duration: 1.1.2003 - 31.12.2006
| Publications |
---|
Heinkel U. ; Mayer C. ; Pleickhardt J. ; Knäblein J. ; Sahm H. ; Webb C. ; Haas W. ; Gossens, Stefan: An Optimized Flow for Designing high-speed, large-scale CMOS ASIC SoCs. In: n.b. (Ed.) : Proc. SAMOS III Workshop: Systems, Architectures, MOdeling, and Simulation (SAMOS III Workshop: Systems, Architectures, MOdeling, and Simulation Samos, Greece July 2003). 2003, pp .. | Haas, W. ; Gossens, Stefan ; Heinkel, U.: Semantics of a Formal Specification Language for Advanced Design and Verification of ASICs (ADeVA). In: n.b. (Ed.) : Proc. 11th E.I.S.-Workshop (11th E.I.S.-Workshop Erlangen April 2003). 2003, pp 51-56. | Heinkel U ; Mayer C. ; Pleickhardt J. ; Knäblein J. ; Sahm H. ; Webb C. ; Haas W. ; Gossens, Stefan: Specification, Design and Verification of Systems-on-Chip in a Telecom Application. In: n.b. (Ed.) : Proc. 11th E.I.S.-Workshop (11th E.I.S.-Workshop, Erlangen April 2003). 2003, pp 45-50. | Gossens, Stefan ; Dal Cin, Mario: Strukturelle Analyse explizit fehlertoleranter Programme. In: n.b. (Ed.) : Proc. 5th Workshop Software-Reengineering (5th Workshop Software-Reengineering Bad Honnef May 2003). 2003, pp .. | Sand, Matthias: Patterns for Model Verification. In: n.b. (Ed.) : Supplement to Proc. HASE 2005: International Symposium on High Assurance Systems Engineering (Ninth IEEE International Sympossium on High Assurance Systems Engineering Heidelberg, Germany 12-14. October 2005). 2005, pp 3-4. | Sand, Matthias: Patternbasierte Verifikation objektorientierter Modelle - Methodik, Semantik und Verfahren. Erlangen-Nürnberg, Friedrich-Alexander-Universität, Ph.D. thesis, 2006 | Gossens, Stefan ; Belli, Fevzi ; Beydeda, Sami ; Dal Cin, Mario: View Graphs for Analysis and Testing of Programs at Different Abstraction Levels. In: IEEE Computer Society (Ed.) : Ninth IEEE International Symposium on High Assurance Systems Engineering (HASE 2005 Ninth IEEE International Symposium on High Assurance Systems Engineering Heidelberg, Germany 12-14 October 2005). 2005, pp 121-130. | Gossens, Stefan ; Dal Cin, Mario: A View-based Control Flow Metric. In: n.b. (Ed.) : Proceedings of IEEE International Computer Software and Applications Conference 2004 (COMPSAC 2004) (IEEE International Computer Software and Applications Conference 2004 (COMPSAC 2004) Hong Kong, China September). 2004, pp -. | Wang F. ; Gossens, Stefan ; Haas W. ; Heinkel U.: Generierung von Plänen für die funktionale Verifikation automatenbasierter Entwürfe. In: n.b. (Ed.) : Proceedings of Dresdner Arbeitstagung Schaltungs- und Systementwurf (DASS'04) (Dresdner Arbeitstagung Schaltungs- und Systementwurf (DASS'04) Dresden April). 2004, pp .. | Gossens, Stefan: Sichtgraphen: Ein Konzept zur gezielten Untersuchung von Kontrollflussstrukturen. Erlangen, Friedrich-Alexander-Universität Erlangen-Nürnberg, Ph.D. thesis, 2004 | Gossens, Stefan ; Dal Cin, Mario: Structural Analysis of Explicit Fault-Tolerant Programs. In: n.b. (Ed.) : Proceedings of IEEE High-Assurance System Engineering Symposium 2004 (HASE 2004) (IEEE High-Assurance System Engineering Symposium 2004 (HASE 2004) Tampa, USA March). 2004, pp .. | Sand, Matthias: Verification and Test of Critical Systems with Patterns and Scenarios in UML. München : TU München. 2004 (TUM-I0415). - Internal report |
Institution: Chair of Computer Science 3 (Hardware Architectures)
|
|
|