Formal specification synthesis using requirements particle networks

Wiwat Vatanawood

dc.contributor.advisor	Wanchai Rivepiboon
dc.contributor.author	Wiwat Vatanawood
dc.contributor.other	Chulalongkorn University. Faculty of Engineering
dc.date.accessioned	2006-08-03T02:16:46Z
dc.date.available	2006-08-03T02:16:46Z
dc.date.issued	2002
dc.identifier.isbn	9741715323
dc.identifier.uri	http://cuir.car.chula.ac.th/handle/123456789/1387
dc.description	Thesis (D.Eng.)--Chulalongkorn University, 2002	en
dc.description.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	en
dc.description.abstractalternative	นำเสนอแผนการเขียนข้อกำหนดรูปนัยของซอฟต์แวร์โดยใช้กฏการตัดสินใจ ที่เกิดขึ้นในระบบเป็นตัวกำหนดข้อกำหนดซอฟต์แวร์ ผู้วิจัยได้นำเสนอสัญลักษณ์ทางกราฟิกที่เรียกว่า เครือข่ายอนุภาคความต้องการ (อาร์พีเอ็น) เพื่อใช้ในการอธิบายเงื่อนไขก่อนและการทำงานที่เป็นส่วนหลักและจำเป็น สำหรับระบบซอฟต์แวร์ที่กำหนดขึ้นด้วยกฏการตัดสินใจ เครือข่ายอาร์พีเอ็นประกอบด้วยกลุ่มของอนุภาคและเส้นเชื่อม เพื่อสร้างแบบจำลองเชิงภาพของกฏการตัดสินใจใดๆ ที่กำหนดขึ้นในช่วงการวิเคราะห์ระบบ งานวิจัยนี้ได้นำเสนอกฏการเปลี่ยนแปลงที่ใช้ในการสังเคราะห์ข้อกำหนดรูปนัย โดยมีโครงข้อกำหนดรูปนัยที่ได้รับการกำหนดขึ้นไว้แล้ว และนำมาใช้งานซ้ำได้อีกระหว่างขั้นตอนการสังเคราะห์ข้อกำหนดรูปนัย ข้อกำหนดรูปนัยที่เหมาะสมจะได้รับการสร้างขึ้นอย่างมีระบบ เพื่อสนองตอบผู้พัฒนาระบบที่มีความรู้พื้นฐานทางคณิตศาสตร์ไม่มาก นักผู้วิจัยได้สาธิตการกำหนดข้อกำหนดรูปนัยที่เขียนด้วยภาษาเซด โดยใช้แผนผังอาร์พีเอ็น การใช้งานของแผนผังอาร์พีเอ็นได้รับการตรวจสอบโดยจัดให้มีการสัมมนาเชิงปฏิบัติการ ผลลัพธ์ที่ได้บ่งชี้ว่าผู้พัฒนาระบบที่มีประสบการณ์ในการเขียน และใช้งานแผนผังการไหลข้อมูลแล้ว จะมีขีดความสามารถในการผลิตแผนผังอาร์พีเอ็นได้ครบถ้วนและมีความสอดคล้อง นอกจากนี้ผู้วิจัยได้แสดงกรณีศึกษาที่ใช้งานแผนผังอาร์พีเอ็น สำหรับกำหนดการทำงานแบบคอมโพสิท ที่ใช้งานในโปรแกรมประยุกต์ที่มีระบบฐานข้อมูลได้
dc.format.extent	2345708 bytes
dc.format.mimetype	application/pdf
dc.language.iso	en	en
dc.publisher	Chulalongkorn University	en
dc.rights	Chulalongkorn University	en
dc.subject	Computer software--Specifications	en
dc.subject	Formal methods (Computer science)	en
dc.subject	Requirements particle networks	en
dc.title	Formal specification synthesis using requirements particle networks	en
dc.title.alternative	การสังเคราะห์ข้อกำหนดรูปนัยโดยใช้เครือข่ายอนุภาคความต้องการ	en
dc.type	Thesis	en
dc.degree.name	Doctor of Philosophy	en
dc.degree.level	Doctoral Degree	en
dc.degree.discipline	Computer Engineering	en
dc.degree.grantor	Chulalongkorn University	en
dc.email.advisor	wanchai.R@chula.ac.th