Research topics
Istvan Majzik
Department of Measurement and Information Systems
Budapest University of Technology and Economics
Dependability
modeling and analysis
An effective design process of a dependable
computer system should include the validation of the architectural choices regarding
the applied fault tolerance techniques (redundancy structures, reconfiguration
strategy etc.). Evaluation of dependability could be supported by the elaboration
of a (stochastic) dependability model that could be solved to get the reliability
and availability measures of the system. These results allow the comparison of
alternative solutions, the identification of dependability bottlenecks and the
estimation of the sensitivity of the system level measures to component attributes.
Three selected publications:
- I. Majzik, G. Huszerl:
Towards
Dependability Modeling of FT-CORBA Architectures
A. Bondavalli, P. Thevenod-Fosse (eds.): Dependable Computing - EDCC4.
In Proc. 4th European Dependable Computing Conference, Toulouse, France, 23-25
October 2002, LNCS 2485, Springer Verlag, Berlin Heidelberg, pp. 121-139,
2002.
The paper presents techniques to
support the dependability modeling and analysis of distributed object-oriented
applications that are designed according to the Fault Tolerant CORBA (FT-CORBA)
specification. First the construction of a high-level dependability model
is described. It is based on the architecture of the application and allows
the analysis of the fault tolerance strategies and properties that are directly
supported by the standard infrastructure. Then a technique to construct a
refined dependability model is presented. It exploits the detailed behavioral
model of the object responsible for replica maintenance. The UML statechart
of this object is transformed to a stochastic Petri net that forms the core
of the dependability model. In this way the designer is allowed to utilize
the full power of statecharts to construct models of application-dependent
replication strategies and recovery policies.
- I. Majzik, A. Pataricza and A.
Bondavalli:
Stochastic
Dependability Analysis of System Architecture based on UML Models
In R. de Lemos, C. Gacek and A. Romanovsky: Architecting Dependable Systems.
LNCS 2677, Springer Verlag, Berlin Heidelberg, pp. 219-244, 2003.
The work in this paper is
devoted to the definition of a dependability modeling and model based evaluation
approach based on UML models. It is to be used in the early phases of the
system design to capture system dependability attributes like reliability
and availability, thus providing guidelines for the choice among different
architectural and design solutions. We show how structural UML diagrams can
be processed to filter out the dependability related information and how a
system-wide dependability model is constructed. Due to the modular construction,
this model can be refined later as more detailed information becomes available.
We discuss the model refinement based on the General Resource Model, an extension
of UML. We show that the dependability model can be constructed automatically
by using graph transformation techniques.
- A. Bondavalli, M. Dal Cin, D.
Latella, I. Majzik, A. Pataricza and G. Savoia:
Dependability
Analysis in the Early Phases of UML Based System Design
International Journal of Computer Systems - Science & Engineering, Vol.
16 (5), Sep 2001, pp. 265-275.
A thorough system specification
is insufficient to guarantee that a computer system will adequately perform
its tasks during its entire life cycle. The early evaluation of system characteristics
like dependability, correctness and performance is necessary to assess the
conformance of the system under development to its targets. This paper presents
the results achieved so far to develop an integrated environment, where design
tools based on the UML (Unified Modeling Language) are augmented with validation
and analysis techniques that provide useful information in the early phases
of system design. Automatic transformations are defined for the generation
of models to capture system behavioral properties, dependability and performance.
Formal
verification
Verification is the activity
of determination, by analysis and test, that the output of each phase of the design
process of a computer system fulfils the requirements of the previous phase. More
informally, verification checks whether "the system was built right", i.e. some
properties of interest (desirable behavior) are satisfied by the current design
(model) of the system. (A complementary task during the design is validation
that checks whether "the right system was built", i.e. the system fits for its
purpose.) Formal verification is a procedure that applies the concepts
and techniques from logic and discrete mathematics to prove that the system (model)
satisfies the required properties.
Three selected publications:
- A. Darvas, I. Majzik, B. Benyó:
Verification
of UML Statechart Models of Embedded Systems
In B. Straube, E.J. Marinissen, Z. Kotasek, O. Novak, J. Hlavicka, R. Ruzicka
(editors): Proc. 5th IEEE Design and Diagnostics of Electronic Circuits and
Systems Workshop (DDECS 2002), April 17-19, Brno, Czech Republic, 2002, pp 70-77
This paper presents a method for
verification of UML statechart models generated in the development process
of embedded systems containing hardware and software components. The method
allows the automated verification of behavioral requirements through model
transformation and application of an off-the-shelf model checker. The transformation
tools have been implemented and the method was applied successfully in the
design verification of an interrupt controller. The paper deals with the details
of the verification method and introduces the application example as well.
- D. Latella, I. Majzik, M. Massink:
Automatic
Verification of a Behavioural Subset of UML Statechart Diagrams Using the SPIN
Model-checker
Formal Aspects of Computing, Volume 11 Issue 6 (Springer Verlag) pp 637-664,
1999
Statechart Diagrams provide a graphical
notation for describing dynamic aspects of system behaviour within the Unified
Modelling Language (UML). In this paper we present a translation from a subset
of UML Statechart Diagrams - covering essential aspects of both concurrent
behaviour, like sequentialisation, parallelism, non-determinism and priority,
and state refinement - into PROMELA, the specification language of the SPIN
model checker. SPIN is one of the most advanced analysis and verification
tools available nowadays. Our translation allows the automatic verification
of UML Statechart Diagrams. The translation is simple, proven correct, and
promising in terms of state space representation efficiency.
- D. Latella, I. Majzik and M.
Massink:
Towards
a Formal Operational Semantics of UML Statechart Diagrams
Proc. FMOODS'99, the Third IFIP International Conference on Formal Methods for
Open Object-based Distributed Systems, Firenze, Italy, pp 331-347, February
1999
Statechart Diagrams are the core
behavioral part of UML, the Unified Modeling Language of object-oriented systems.
UML is a semi-formal language, with a precisely defined syntax and static
semantics but with an only informally specified dynamic semantics. UML
Statechart Diagrams differ from classical, Harel Statecharts, for which some
formalizations and results are available in the literature. This paper
sets the basis for the development of a formal semantics for UML Statechart
Diagrams based on Kripke structures. This forms the first step towards model
checking of UML Statechart Diagrams. We follow the approach proposed
by Mikk and others: we first map Statechart Diagrams to the intermediate format
of extended hierarchical automata and then we define an operational semantics
for extended hierarchical automata. We prove a number of properties of such
semantics which reflect the design choices of UML Statechart Diagrams.
Formal analysis
of safety-critical systems
According to experiences, specification
errors like incompleteness and inconsistency may cause deficiencies
or even malfunctions leading to accidents in safety-critical computer systems.
Completeness with respect to an embedded control system means that a response
is specified for every possible input sequence, including also timing variations
(early, lately, delayed etc. inputs). Consistency implies that there are no conflicting
requirements and no (unintentional) nondeterminism.
Three selected publications:
- A. Pataricza, I. Majzik, G. Huszerl,
Gy. Várnai:
UML-based
Design and Formal Analysis of a Safety-Critical Railway Control Software Module
In G. Tarnai and E. Schnieder (eds.): Formal Methods for Railway Operation and
Control Systems (Proceedings of Symposium FORMS-2003, Budapest, Hungary, May
15-16), pp.125-132, 2003, L' Harmattan, Budapest.
A new equipment of safety relevance
has been developed to upgrade ageing relay-based railway interlocking systems
in Hungary. In course of the design process formal methods have been used
in the development of a module realising a well-separable function of the
system. Namely, the UML-based design process was extended by model based analysis
and validation. The first kind of analysis checked the completeness and consistency
of the behavioural description of the module. In the subsequent phases, the
functional design was enriched by modelling the potential faults and their
effects. This kind of extension allowed the analysis of the error propagation
and testability.
- Zs. Pap, I. Majzik, A. Pataricza:
Checking
General Safety Criteria on UML Statecharts
20th International Conference on Computer Safety, Reliability and Security 2001
(SafeComp 2001), Proceedings (Springer Lecture Notes in Computer Science, No.
2187), pp. 46-55, September 25-27, 2001.
This paper describes methods and
tools for automated safety analysis of UML statechart specifications. The
general safety criteria described in the literature are reviewed and automated
analysis techniques are proposed. The techniques based on OCL expressions
and graph transformations are detailed and their limitations are discussed.
To speed up the checker methods, a reduced form for UML statecharts is introduced.
Using this form, the correctness and completeness of some checker methods
can be proven. An example illustrates the application of the tools developed
so far.
- Zs. Pap, I. Majzik, A. Pataricza
and A. Szegi:
Completeness
and Consistency Analysis of UML Statechart Specifications
In: Proceedings of the DDECS 2001 Workshop, April 2001, Győr, Hungary, pp. 83-90.
This paper describes methods and
tools for automatic safety analysis of UML statechart specifications. Two
types of analysis are presented. The first one checks completeness and consistency
based on the static structure of the specification, thus it does not requires
the generation of the reachability graph. Accordingly, this method scales
up well to large systems. The second one performs dynamic analysis by checking
safety related reachability properties with the help of a model checker. It
is restricted to core critical parts of the system. Two approaches of the
implementation of the static checking are discussed. The use of the tools
is presented by a case study.
Quantitative
dependability analysis
Formal modeling and analysis techniques
of modern computer controlled systems become more and more important. In critical
systems like transportation or production systems not only the functional correctness,
but also the reliability, availability and performability have to be analyzed.
The analysis is especially important in the early design phases, since modifications
and re-design are costly if an inadequacy is detected in the later phases of the
development. Our work is focused on the non-functional quantitative analysis of
the UML behavioral models of embedded systems. The analysis is based on a transformation
from UML statechart models enriched with timing and stochastic information to
Stochastic Petri nets.
Three selected publications:
- Huszerl G., Majzik I., Pataricza
A., K. Kosmidis, M. Dal Cin:
Quantitative
Analysis of UML Statechart Models of Dependable Systems
The
Computer Journal, Vol 45(3), May 2002, pp. 260-277, ISSN: 0010-4620
The paper introduces a method which
allows quantitative dependability analysis of systems modeled by using the
Unified Modeling Language (UML) statechart diagrams. The analysis is performed
by transforming the UML model to stochastic reward nets (SRNs). A large subset
of statechart model elements is supported including event processing, state
hierarchy and transition priorities. The transformation is presented by a
set of SRN patterns. Performance-related measures can be directly derived
using SRN tools, while dependability analysis requires explicit modeling of
erroneous states and faulty behavior.
- G. Huszerl and I. Majzik:
Modelling
and Analysis of Redundancy Management in Distributed Object-Oriented Systems
by Using UML Statecharts
In: Proc. of the 27th Euromicro Conference, pp. 200-207., Warsaw, Poland, 4-6.
September 2001.
The paper presents techniques that
enable the modeling and analysis of redundancy schemes in distributed object-oriented
systems. The replication manager, as core part of the redundancy scheme, is
modeled by using UML statecharts. The flexibility of the statechart-based
modeling, which includes event processing and state hierarchy, enables an
easy and efficient modeling of replication strategies as well as repair and
recovery policies. The statechart is transformed to a Petri-net based dependability
model, which also incorporates the models of the replicated objects. By the
analysis of the Petri-net model the designer can obtain reliability and availability
measures that can be used in the early phases of the design to compare alternatives
and find dependability bottlenecks. Our approach is illustrated by an example.
- Huszerl G., Majzik I.:
Quantitative
Analysis of Dependability Critical Systems Based on UML Statechart Models
Proc. HASE'2000, the Fifth IEEE International High-Assurance Systems Engineering
Symposium, Albuquerque, New Mexico, pp 83-92, 2000.
The paper introduces a method which
allows quantitative performance and dependability analysis of systems modeled
by using UML statechart diagrams. The analysis is performed by transforming
the UML model to Stochastic Reward Nets (SRN). A large subset of statechart
model elements is supported including event processing, state hierarchy and
transition priorities. The transformation is presented by a set of SRN design
patterns. Performance measures can be directly derived using SRN tools, while
dependability analysis requires explicit modeling of erroneous states and
faulty behavior.
Concurrent
error detection
As the experiments have shown, a high
portion of failures results from transient faults. They are hard to be
avoided by careful design (fault avoidance) and testing during the manufacturing
process (fault removal), thus fault tolerance techniques are needed to improve
the dependability of the system. Since the dependability of the system is especially
sensitive to undetected or mishandled transient faults, the application of efficient
error detection techniques is of utmost interest. Moreover, in parallel computing
systems running long, computing intensive applications early error detection is
a vital requirement. Regularly scheduled off-line tests are usually too time consuming,
without being able to detect transient faults, therefore concurrent, on-line error
detectors are used.
One example of concurrent error detectors is a watchdog processor. It is
a relatively small and simple coprocessor used to perform concurrent system-level
error detection by monitoring the behavior of a main processor. The watchdog is
provided with some information about the state of the processor or process to
be checked on the system (instruction and/or data) bus. Errors detected by the
WP are signaled towards the checked processor or any external supervisory unit
responsible for error treatment and recovery.
Three selected publications:
- I. Majzik, J. Jávorszky, A. Pataricza
and E. Selényi:
Concurrent
Error Detection of Program Execution Based on Statechart Specification
Proc. EWDC-10, the 10th European Workshop on Dependable Computing, May 6-7,
Vienna, Austria pp 181-185, 1999
In common procedural and object-oriented
programming languages the control flow of a program is a hierarchical structure.
Concurrent error detectors proposed in previous works were able to check the
sequence of statements in procedures and the procedure return addresses, but
the problem of checking the allowed sequence of procedure calls and inter-process
synchronization remained unsolved. In this paper we propose an approach of
checking the higher-level program control flow using reference information
based on UML statechart specification.
- Majzik, I.; Hohl, W.; Pataricza,
A.; Sieh, W.:
Multiprocessor
Checking Using Watchdog Processors
International Journal of Computer Systems - Science & Engineering, Vol.
11, No. 5, pp 123-132, 1996
A new control flow checking scheme
is presented, based on assigned-signature checking using a watchdog processor.
This scheme is suitable for a multitasking, multiprocessor environment. The
hardware overhead is comparatively low because of three reasons: first, hierarchically
structured, the scheme uses only a single watchdog processor to monitor multiple
processes on multiple processors. Second, as an assigned-signature scheme,
it does not require monitoring the instruction bus of the processors. Third,
the run-time and reference signatures are embedded into the checked program;
thus, in the watchdog processor neither a reference database nor a time-consuming
search and compare engine is required.
- Majzik, I.:
Software
Diagnosis Using Compressed Signature Sequences
Periodica Polytechnica Ser. Electrical Engineering, Vol. 40, No. 2, pp 87-103,
1996
Software diagnosis can be effectively
supported by one of the concurrent error detection methods, the application
of watchdog processors (WP). A WP, as a coprocessor, receives and evaluates
signatures assigned to the states of the program execution. After the checking,
the watchdog stores the run-time sequence of signatures which identify the
statements of the program. In this way, a trace of the statements executed
before the error is available. The signature buffer can be effectively utilized
if the signature sequence is compressed. In the paper, two real-time compression
methods are presented and compared. The general method uses predefined dictionaries,
while the other one utilizes the structural information encoded in the signatures.