The statecharts formalism is a graphical language that has been successfully used for specifying reactive and real-time systems. In this dissertation, we discuss two fundamental requirements engineering problems in the development of reactive and real-time systems based on statecharts: verification and testing. First we present a symbolic model checking approach to formal verification of statecharts. Symbolic model checking is a proven successful technology for the automatic verification of finite state machines. We show how CTL model checking, RTCTL model checking, and the quantitative analysis can be applied to statecharts and discuss how they can be implemented in the symbolic model checker SMV. Our approach enables the verification of properties ranging from temporal properties of safety and liveness to time-bounded properties and the computation of several timing information for reactive and real-time systems. Second we present a specification-based testing method for reactive systems using statecharts. We show that statecharts can be conservatively transformed into flow graphs modeling the flow of both control and data in statecharts. The transformation enables the application of conventional data flow analysis techniques to the selection of test sequences from statecharts. The resulting set of test sequences provides the capability of determning whether an implementation establishes the desired flow of data prescried in statecharts.
Statecharts는 유한 상태 기계를 기반으로 하는 명세언어로서, 반응적 시스템이나 실시간 시스템의 명세에 널리 사용되고 있다. 본 논문에서는 statecharts를 기반으로 하여 반응적 시스템이나 실시간 시스템을 개발할 때에 요구사항 공학에서 중요한 두가지 문제점인 검증과 테스팅에 대하여 논의한다. 먼저 본 논문은 statecharts로 작성된 요구사항 명세를 symbolic model checking을 통하여 정형적으로 검증할 수 있는 방법을 제안한다. 구체적으로 본 논문에서는 CTL 모델 검사 방법, RTCTL 모델 검사 방법, 그리고 정량적 검사 방법을 statecharts에 적용하며, 이들 방법들이 어떻게 효율적으로 SMV를 통하여 구현되는지를 보여준다. 이들 방법들은 statecharts의 여러가지 시간적인 성질들, 예를 들어 간단한 형태의 안전성에서 복잡한 형태의 시간 제한적인 성질들, 그리고 두개의 상태간의 최소, 최대 시간등의 유용한 시간 관련 성질들을 분석하고 검증할 수 있게 한다. 둘째로 본 논문에서는 statecharts를 사용하는 반응적 시스템의 명세 기반 테스팅 방법을 제안한다. 먼저 우리는 statecharts를 프로그래밍 언어 연구에서 많이 사용되는 제어 및 자료 흐름도로 변환하는 방법을 제안하며, 이 변환 방법의 올바름을 오토마타의 언어 이론을 사용하여 증명한다. Statecharts에서 흐름도로의 변환을 통하여 우리는 기존의 자료 석 기법을 statecharts에 적용하 수 있으며, 이를 이용하여 테스트 케이스를 생성할 수 있게 된다. 이렇게 생성된 테스트 케이스는 statecharts로 작성된 명세에서의 자료흐름이 실제로 제대로 구현되어 있는지를 테스팅할 때에 유용하게 쓰일 수 있다.
