Two notable characteristics of real-time parallel programs are constraints on the timing behaviors and concurrency among tasks. Timing behaviors and concurrency are associated with uncertainty which may incur subtle yet critical timing and communicating errors. In this thesis, we deal with three kinds of uncertainty in real-time parallel programs and their specifications - timing uncertainty, nondeterminacy, and incompleteness. In particular, we describe the implications of the uncertainty over the verification phase and suggest a few ways of testing and verifying real-time parallel programs with uncertainty.
Timing aspects of real-time programs are affected by such factors as external interfaces and underlying platforms. Since it is almost impossible to predict and/or measure their timing behaviors precisely, we propose a method of coping with such timing uncertainty in a formal fashion by incorporating fuzzy concepts into the timing model of duration calculus formalism. Semantics and proof systems for fuzzy duration calculus are also defined and illustrated using simple examples. Timing constraints on real-time programs can be verified against the fuzzy duration formulas based on the proof systems. Compared to the classical formalism, fuzzy duration calculus allows us to capture the vagueness of state intervals using fuzzy numbers. To demonstrate the effectiveness of the proposed ideas, a part of nuclear power plant control system is specified and verified using the fuzzy duration calculus.
The sequence of interactions among concurrent tasks can change for reasons such as relative progress of tasks and communication delay. Uncertainty in the interaction sequences results in the nondeterminacy of parallel programs. Selective Instrumentation, a reproduction method with minimal probe effects, is suggested in this thesis to handle the difficulties associated with nondeterminacy --- non-reproducibility, probe effects and the space overhead. In order to minimize probe effects and guarantee reproducibility, we employ a static analysis technique which identifies the statements in parallel programs where nondeterminacy might occur. An MHB model was devised to catch permanent ordering relations among statements and algorithms are developed to locate nondeterminacy based on the MHB model. By inserting probes only into the locations marked in the analysis phase, we can guarantee reproducibility with minimal probe effects and low space overhead.
It is usually the case in practice that only a partial and nondeterministic specification exists for the testing purpose. A parallel program may exercise excessive sequences which cannot be induced from a partial specification. On the other hand, a certain type of nondeterminacy may be discarded in a program although it is accommodated in a nondeterministic specification. This implies that the equivalence relation, which requires a specification and a program to encompass the same set of synchronization sequences, is not well-suited for testing parallel programs against incomplete specifications. We define new conformance relations - behavioral conformance and nondeterminacy conformance - and suggest a testing framework which supports the module-level testing of parallel programs using Message Sequence Charts specifications. After extracting the sequencing constraints from an MSC specification, a state machine-like test driver is constructed for the module under test. Behavioral conformance and nondeterminacy conformance between the module and the MSC specification can be determined by executing the module together with the test driver in a nondeterministic and deterministic manner, respectively.
In order to investigate the effectiveness of our testing and debugging methods, a prototype environment is implemented and applied to a telephone switching system example.'
80년대부터 병렬성을 지원하는 하드웨어 및 네트웍의 보급이 확산되고 다양한 내포 시스템(embedded system)에 컴퓨터가 도입됨에 따라 실시간 병렬 소프트웨어의 사용이 증가되는 추세에 있다. 특히 최근의 실시간 병렬 소프트웨어는 원자력 발전소 관리 시스템, 유선 및 무선 통신 소프트웨어, 항공기 제어 시스템, 국방 무기 체계 시스템 등 고신뢰성을 요구하는 분야에 많이 사용되고 있기 때문에 철저한 검증 및 테스팅 기법이 요구되고 있다.
실시간 병렬 프로그램이 가지는 두 가지 독특한 특성은 시간 제약 조건과 태스크 간의 병행성이다. 검증 및 테스팅 관점에서 볼 때 이 두 가지 특성은 불확정성과 연관되어 있기 때문에 수행 중에 미묘한 시간 오류나 상호작용 오류를 유발할 수 있다. 이 논문에서는 실시간 병렬 프로그램 및 그 명세에 내포된 세가지 종류의 불확정성-시간 불확정성, 비결정성, 불완전성-을 테스팅 및 검증 단계에서 다루는 방법을 제시한다. 먼저, 세가지 종류의 불확정성을 구체적으로 설명하고 각각이 검증 단계에 어떤 영향을 끼치는지를 기술하며 불확정성을 가진 실시간 병렬 프로그램의 시간 오류와 상호작용 오류를 검증하고 테스팅하는 방법들을 제안한다.
실시간 프로그램의 시간 특성은 프로그램의 수행 환경이나 외부 인터페이스, 스케쥴링 알고리즘 등에 의해서 영향을 받기 때문에 수행할 때마다 조금씩 변화한다. 따라서 프로그램의 시간 특성을 정확하게 측정하거나 예측하는 것이 매우 어려워지는데 이를 시간 불확정성이라 한다. 시간 불확정성을 가지는 실시간 프로그램의 시간 오류를 검출하기 위해서 우리는 정형적 기법을 사용한다. 기존의 정형적 모델은 시스템의 시간 특성을 실수(real number)로 표현하기 때문에 시간 불확정성을 효과적으로 표현하지 못했는데 여기서는 duration calculus의 시간 모델에 퍼지 개념을 도입하여 fuzzy duration calculus를 제시함으로써 시간 불확정성을 모델에 반영할 수 있도록 하였다. 또한 fuzzy duration calculus에 대한 정형적 의미와 검증 시스템을 새롭게 정의함으로써 퍼지 개념이 도입된 모델에 대해서 추론을 통한 증명을 지원하며 이 기법을 실제 원자력 발전소 제어 시스템의 일부분에 적용해 봄으로써 효용성을 확인하였다.
병렬 프로그램을 구성하는 태스크들은 수행 중에 메시지나 공유 변수를 이용해서 상호작용 하는데 이 상호작용 순서는 각 태스크의 진행 정도, 통신 지연 시간, 스케쥴링 알고리즘 등에 의해서 영향을 받기 때문에 불확정성을 가진다. 이와 같은 상호작용 불완전성은 프로그램의 비결정성을 유발한다. 이 논문에서는 비결정적 병렬 프로그램의 상호작용 오류를 검출할 때 발생하는 문제점들을 해결하기 위해서 selective instrumentation 기법을 제시한다. 비결정적 프로그램 내의 상호작용 오류를 검출하려면 탐침 효과와 메모리 오버헤드를 최소화 하면서 프로그램의 재수행성을 보장해야 한다. 기존의 기법들은 태스크 간에 상호작용이 발생할 때마다 탐침 코드가 수행되어 태스크 간 상호작용 순서를 기록한다. 반면에 selective instrumentation 기법에서는 정적 분석을 통해서 비결정성을 유발할 수 있는 문장들을 미리 검출하고 검출된 문장에 대해서만 탐침을 삽입하기 때문에 재수행성을 보장하면서도 탐침의 수행 횟수와 수행 시간이 적어지고 결과적으로 탐침효과 및 메모리 오버헤드가 줄어든다.
병렬 프로그램에 대한 테스팅은 명세에 포함된 상호작용 시퀀스와 프로그램에 구현된 상호작용 시퀀스가 서로 일치하는지를 검사하는데 중점을 둔다. 기존의 대부분의 테스팅 기법들은 명세와 프로그램 간의 동치 관계를 기반으로 발전되었으며 이는 명세에 포함된 시퀀스와 프로그램에 구현된 시퀀스가 동일함을 의미한다. 그러나 산업계에서는 불완전하며 비결정적인 명세를 사용하는 경우가 많다. 명세가 불완전한 경우에 프로그램에는 명세에 나타나지 않은 상호작용 시퀀스가 추가될 수 있으며 반대로 명세가 비결정적인 경우에 명세에 나타난 시퀀스 중에 일부는 프로그램에 나타나지 않을 수도 있다. 따라서 불완전하며 비결정적인 명세를 이용해서 테스팅할 때 동치 관계와 다른 새로운 관계가 필요하며 이 논문에서 우리는 두 가지 새로운 관계 - behavioral conformance, nondeterminacy conformance - 를 제시하였다. 또한, 메시지 순차도로 작성된 명세와 병렬 프로그램 간의 합치성을 이 두 가지 관계를 기반으로 테스팅할 수 있는 방법을 제시하였다. 메시지 순차도로부터 이벤트 간의 순서 제약 조건을 추출하고 이 조건을 이용해서 주어진 프로그램에 대한 테스트 드라이버를 구축하며 테스트 드라이버와 프로그램을 비결정적인 방법으로 동시에 수행해서 behavioral conformance를 테스팅하고 결정적인 방법으로 수행해서 nondeterminacy conformance를 테스팅한다.
논문에서 제시한 테스팅 및 디버깅 기법의 효용성을 보이기 위해서 테스팅 및 디버깅 도구가 구현되었으며 사설 교환기 제어 프로그램의 테스팅 및 디버깅에 실제로 적용되었다.
