@techreport{oai:ipsj.ixsq.nii.ac.jp:00030194,
 author = {菅原, 佳菜 and 高橋, 薫 and Kana, Sugawara and Kaoru, Takahashi},
 issue = {30(1997-PRO-018)},
 month = {Mar},
 note = {情報処理システムの大規模化・複雑化に伴い，信頼性の高いシステムを効率よく設計するための形式的仕様記述法の必要性が高まっている．そのような記述法の一つとして，情報処理システムがその果たす機能によって記述できること，また個々の機能がその機能を実行するための前提条件，入力，出力，事後条件によって記述できることに着目した，命題論理に基づいた要求記述法と状態遷移システムによるその意味記述法が提案されている．本論文では，従来単一システムを対象としていた上記の要求記述法を，いくつかのサブシステムから成る並行システムに拡張する．そのために，サブシステム毎の機能要求記述，およびその集まりとしての並行システム機能要求記述を提案する．更に，これら機能要求記述から形式仕様としての状態遷移システムを合成する方法についても述べる．, As information processing systems become large and complex, formal description methods are needed for specification of systems and their efficient and reliable designs. Since information processing systems can be described by some executed functions and each function for execution can be described by a pre-condition to be satisfied before execution, input, output and a post-condition to be satisfied after execution, a description method based on propositional logic and its semantic description method by a state transition system have been proposed. In this paper, we extend the above mentioned description method whose target is a dingle system so that a concurrent system consisting of some subsystems can be handled. For this purpose, we give a functional requirement description method of each subsystem and a concurrent system as a collection of subsystems. We also propose a method to synthesize a state transition system as a formal specification from a functional requirement description.},
 title = {命題論理に基づいた並行システムの仕様記述},
 year = {1998}
}