从命题逻辑的需求描述到状态转移图的形式规格

FORM THE REQUIREMENT DESCRIPTION OF PROPOSITIONAL LOGIC TO FO RMAL SPECIFICATION OF STATE TRANSITION SYSTEM

信息处理系统的大规模化和复杂化 ,需要有效设计高可靠性系统的形式化的规格描述方法 .在通信系统中 ,前期设计阶段就要考虑系统变更频繁的情况 ,使得部分变更不要影响到系统的整体规格 .本文针对以上功能 ,提出了基于命题逻辑的信息处理系统的新的需求描述方法 .描述了通过使用逻辑 Petri Net( L PN) ,把命题逻辑的需求描述变换成状态转移图的过程 .并且给出了由 L PN自动生成状态转移图的算法 .

Information processing systems becoming large and complex, Formal desc ription methods are needed for specification of systems and their efficient and reliable designs. During the initial phase of design, it is necessary to modify or change system requirements which may influence the whole design specification . In this paper , we propose a new description method of information processing systems based on propositional logic. We depict the whole process of change the requirements description of propositional logic into state transition system by using logical PetriNet (LPN), and state algorithm for synthesizing state trans ition system by LPN.