Research topics of István Majzik
Table of contents
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: Modeling 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.
