Connectors as designs: Modeling, refinement and test case generation

详细信息	查看全文 | 推荐本文 |

• 作者：Sun Meng^a ; ^b ; ^{sunmeng@math.pku.edu.cn} ; Farhad Arbab^b ; ^{Farhad.Arbab@cwi.nl} ; Bernhard K. Aichernig^c ; ^{aichernig@ist.tugraz.at} ; L膬cr膬mioara A艧tef膬noaei^b ; ^{L.Astefanoaei@cwi.nl} ; Frank S. de Boer^b ; ^{F.S.de.Boer@cwi.nl} ; Jan Rutten^b ; ^{Jan.Rutten@cwi.nl}
• 关键词：Connector ; Reo circuits ; Timed data sequence ; Design ; Refinement ; Test case generation
• 刊名：Science of Computer Programming
• 出版年：2012
• 期刊代码：108_01676423
• 类别：cp
• 出版时间：1 July, 2012
• 卷：77
• 期：7-8
• 页码：799-822
• 文件大小：433 K

摘要

Over the past years, the need for high-confidence coordination mechanisms has intensified as new technologies have appeared for the development of service-oriented applications, making formalization of coordination mechanisms critical. Unifying Theories of Programming (UTP) provide a formal semantic foundation not only for programming languages but also for various expressive specification languages. A key concept in UTP is design: the familiar pre/post-condition pair that describes a contract. In this paper we use UTP to formalize Reo connectors, whereby connectors are interpreted as designs in UTP. This model can be used as a semantic foundation for proving properties of connectors, such as equivalence and refinement relations between connectors. Furthermore, it can be used as a reference document for developing tool support for Reo, such as test case generators. A fault-based method to generate test cases for component connectors from specifications is also provided in this paper. For connectors, faults are caused by possible errors during the development process, such as wrongly used channels, missing or redundant subcircuits, or circuits with wrongly constructed topology. We give test cases and connectors a unifying formal semantics by using the notion of design in UTP, and generate test cases by solving constraints obtained from a specification and a faulty implementation. A prototype serves to demonstrate the automatization of the approach.