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:

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:

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:

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:

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:

Istvan Majzik, 2003.