Towards formal open standards: formalizing a standard’s requirements

详细信息    查看全文

• 作者：Konstantinos Barlas ; Eleni Berki…
• 关键词：Open standards ; Formal methods ; Formal specification ; Rich Site Summary (RSS)v2.0 protocol ; CafeOBJ
• 刊名：Innovations in Systems and Software Engineering
• 出版年：2017
• 出版时间：March 2017
• 年：2017
• 卷：13
• 期：1
• 页码：51-66
• 全文大小：
• 刊物类别：Computer Science
• 刊物主题：Software Engineering; Computing Methodologies; Computer Applications;
• 出版者：Springer London
• ISSN：1614-5054
• 卷排序：13

文摘

Open standardization seems to be very popular among software developers as it simplifies the standard’s adoption by the software engineering. Formal specification methods, while very promising, are being adopted slowly as the industry seems to have little motivation to move into this territory. In this paper the authors present (1) the idea of applying formal specification techniques to open standards’ specifications, and (2) an example of a formal specification of the Rich Site Summary (RSS) v2.0 open standard. The authors provide evidence for the advantages of the open standards formal specification over natural language documentations: formal specifications are more concise, less ambiguous, more complete with respect to the original documentation and, when using certain kinds of specification languages, executable and reusable as they support module inheritance. The merging of formal specification methods and open standards allows (1) a more concrete standard design; (2) an improved understanding of the environment under design; (3) an enforced certain level of precision into the specification, and also (4) provides software engineers with extended property checking/verification capabilities, especially if they opt to use any algebraic specification language. The authors showcase how the RSS standard can be formally specified using an algebraic specification language and demonstrate how can that be beneficial.