Chulalongkorn University Theses and Dissertations (Chula ETD)

Formal specification synthesis using requirements particle networks

Other Title (Parallel Title in Other Language of ETD)

การสังเคราะห์ข้อกำหนดรูปนัยโดยใช้เครือข่ายอนุภาคความต้องการ

Year (A.D.)

2002

Document Type

Thesis

First Advisor

Wanchai Rivepiboon

Faculty/College

Faculty of Engineering (คณะวิศวกรรมศาสตร์)

Degree Name

Doctor of Philosophy

Degree Level

Doctoral Degree

Degree Discipline

Computer Engineering

DOI

10.58837/CHULA.THE.2002.1556

Abstract

An alternative scheme to formal software specification is explicitly proposed. In our approach, a formal software specification is formally defined as a set of decision rules performed by a software system. We propose a set of graphical notations called Requirements Particle Network (RPN), to describe the essential preconditions and operations needed by a software system according to the decision rules. A RPN consists of a set of particles and edges to construct a visual model of a decision rule during the software analysis phase. In addition, a number of transformation rules are proposed to perform the formal specification synthesis. A set of predefined formal requirements particle definitions is written in prior and reused during the transformation steps. A developer is provided a practical mean to write a formal specification with a brief experience in mathematical background. In this research, we demonstrate the Z formal specification synthesis using RPN. The usability of the RPN approach is investigated by conducting a workshop. The result indicates that a developer with experience in writing data flow diagram is capable to produce a complete and consistent RPN. Moreover, we show a case study of applying RPN to construct a composite operation to be used in database applications

Other Abstract (Other language abstract of ETD)

นำเสนอแผนการเขียนข้อกำหนดรูปนัยของซอฟต์แวร์โดยใช้กฏการตัดสินใจ ที่เกิดขึ้นในระบบเป็นตัวกำหนดข้อกำหนดซอฟต์แวร์ ผู้วิจัยได้นำเสนอสัญลักษณ์ทางกราฟิกที่เรียกว่า เครือข่ายอนุภาคความต้องการ (อาร์พีเอ็น) เพื่อใช้ในการอธิบายเงื่อนไขก่อนและการทำงานที่เป็นส่วนหลักและจำเป็น สำหรับระบบซอฟต์แวร์ที่กำหนดขึ้นด้วยกฏการตัดสินใจ เครือข่ายอาร์พีเอ็นประกอบด้วยกลุ่มของอนุภาคและเส้นเชื่อม เพื่อสร้างแบบจำลองเชิงภาพของกฏการตัดสินใจใดๆ ที่กำหนดขึ้นในช่วงการวิเคราะห์ระบบ งานวิจัยนี้ได้นำเสนอกฏการเปลี่ยนแปลงที่ใช้ในการสังเคราะห์ข้อกำหนดรูปนัย โดยมีโครงข้อกำหนดรูปนัยที่ได้รับการกำหนดขึ้นไว้แล้ว และนำมาใช้งานซ้ำได้อีกระหว่างขั้นตอนการสังเคราะห์ข้อกำหนดรูปนัย ข้อกำหนดรูปนัยที่เหมาะสมจะได้รับการสร้างขึ้นอย่างมีระบบ เพื่อสนองตอบผู้พัฒนาระบบที่มีความรู้พื้นฐานทางคณิตศาสตร์ไม่มาก นักผู้วิจัยได้สาธิตการกำหนดข้อกำหนดรูปนัยที่เขียนด้วยภาษาเซด โดยใช้แผนผังอาร์พีเอ็น การใช้งานของแผนผังอาร์พีเอ็นได้รับการตรวจสอบโดยจัดให้มีการสัมมนาเชิงปฏิบัติการ ผลลัพธ์ที่ได้บ่งชี้ว่าผู้พัฒนาระบบที่มีประสบการณ์ในการเขียน และใช้งานแผนผังการไหลข้อมูลแล้ว จะมีขีดความสามารถในการผลิตแผนผังอาร์พีเอ็นได้ครบถ้วนและมีความสอดคล้อง นอกจากนี้ผู้วิจัยได้แสดงกรณีศึกษาที่ใช้งานแผนผังอาร์พีเอ็น สำหรับกำหนดการทำงานแบบคอมโพสิท ที่ใช้งานในโปรแกรมประยุกต์ที่มีระบบฐานข้อมูลได้

Link to Full Text

Share

COinS