• 作者： 李允中; 潘健一; 薛念林; 黃為德
• 作者服務機構： 國立中央大學資訊工程研究所
• 中文摘要： 在本論文中，我們提出了使用Z當作正規語言來表達傑克森系統發展方法之需求規格（稱之為JSDZ），其中JSD可視為一個可幫助分析問題領域的機制。在JSDZ方法中，傑克森系統發展方法中的功能處理元（function process )是由運算框架（operation schema）來表示。把一個模式處理元（model process）當作是一個主動實體（active entity）來看待。而主動實體需要一個運算（operation），這個運算能夠產生出新的成員（instance）而加入現有的成員集中。因此，我們把一個模式處理元轉換成一個狀態框架，而且其相關的運算轉換成為運算框架，並且加上一個能夠由運算框架所更改的成員集。結構圖方面則先轉換成狀態轉移圖再轉換成相關的Z規格。程序之問基數（cardinality）關係的表示方法是根據合併（rough merge)表示成Z符號的觀念。我們將以一個租車系統來說明這些轉換。這種結合傑克森系統發展方法與Z正規化規格，使其兼具了圖形表示與正規語意表示的方式，主要是提供兩個優點。首先，JSD規格可視為幫助推導出Z正規化規格的結構化機制貢獻是提供有系統的方法來產生兼具有結構化及正規化的需求規格。
• 英文摘要： In this paper, we propose the use of Z as the formal notation to express Jackson System Development(JSD) specifications (called JSDZ)，where JSD serves as a mechanism to aid analysis of problem domains．A function process in JSD specifications is manifested by an operation schema. A model process is treatedas an active entity that requires an operation on its data store to add a new instance to the collection ofexisting instances．The model process is, thus，translated into a state schema, and its related operationsare converted into the operation schemas with instances set that can be modified by the operations．Astructured diagram is transformed into a state transition diagram and then converted into its Z specificationsCardinality relationships between processes are translated into Z notations based upon the notion of roughmerge. These transformation rules are illustrated using the problem domain of the Car-Rental System.The bringing together of diagrammatical and text elements of JSD specifications in Z notations offerstwo major benefits．First, JSD specifications can be seen both as a structuring mechanism that helps inderiving Z specifications and as a preliminary step that assists in ascertaining the clients requirements.Second, Z specifications make it easier to identify omissions or errors．
• 中文關鍵字： formal specifications; informal methods; Jackson System Development(JSD); methods integration; Z
• 英文關鍵字： --