Program synthesis for stepwise satisfiable specification of reactive system

Reactive system, such as operating systems or elevator control systems, is a system which ideally never terminates and is intended to maintain some interaction with environ ment. In previous researches, a reactive system specification is required to satisfy realizability for synthesizing a program from it. A specification is realizable if and only if there exists a system which satisfies the specification no matter how the environment behaves. However, many of actual reactive system specifications do not satisfy realizability and there exist actual reactive system programs of such specifications. In this paper, we discuss realizability property of actual reactive system specifications and show that stepwise satisfiability is a property which actual reactive system specifications have to satisfy. This paper also presents a synthesis procedure of reactive system programs from stepwisely satisfiable specifications. By this procedure, we can synthesize prototype programs from an imperfect specification. It is useful to synthesize prototype programs in the middle of describing a specification because prototype programs give useful information for testing or revising the specification. Thus, the procedure in this paper is useful for system specification revision.