%0 Journal Article %1 tsai00formal %A Tsai, Jeffrey %A Xu, Kuang %D 2000 %J Annals of Software Engineering %K research.cs.softeng info.refs.journals.ansoft research.cs.softeng.formal %N 1 %P 207--223 %T A comparative study of formal verification techniques for software architecture specifications %U http://dx.doi.org/10.1023/A:1018960305057 %V 10 %X Abstract  With the rapid growth of network computing, the demand for large�?scale and complex software systems has increased dramatically.However, the development of large�?scale and complex software systems is much more difficult and error prone. This is due tothe fact that techniques and tools for assuring the correctness and reliability of software systems lag far behind the increasinggrowth in size and complexity of software systems. The concept of software architecture has recently emerged as a new wayto improve our ability to effectively construct and maintain large�?scale complex software systems. The architecture baseddevelopment of software systems focuses on the architectural elements and their overall interconnection structure. SeveralArchitectural Definition Languages (ADLs) have been proposed for specifying domain specific or general purpose architectures.On the other hand, formal verification is rapidly becoming a promising and automated method to ensure the accuracy and correctnessof software systems. In this paper, we survey several architecture description languages and formal verification methods.We present an environment to conduct experiments to study the performance of five different verification tools on softwarearchitecture specifications. Based on these experiments, we are able to compare the efficiency of these verification toolsin verifying certain software property.

@article{tsai00formal, abstract = {Abstract  With the rapid growth of network computing, the demand for large�?scale and complex software systems has increased dramatically.However, the development of large�?scale and complex software systems is much more difficult and error prone. This is due tothe fact that techniques and tools for assuring the correctness and reliability of software systems lag far behind the increasinggrowth in size and complexity of software systems. The concept of software architecture has recently emerged as a new wayto improve our ability to effectively construct and maintain large�?scale complex software systems. The architecture baseddevelopment of software systems focuses on the architectural elements and their overall interconnection structure. SeveralArchitectural Definition Languages (ADLs) have been proposed for specifying domain specific or general purpose architectures.On the other hand, formal verification is rapidly becoming a promising and automated method to ensure the accuracy and correctnessof software systems. In this paper, we survey several architecture description languages and formal verification methods.We present an environment to conduct experiments to study the performance of five different verification tools on softwarearchitecture specifications. Based on these experiments, we are able to compare the efficiency of these verification toolsin verifying certain software property.}, added-at = {2009-06-25T16:50:50.000+0200}, author = {Tsai, Jeffrey and Xu, Kuang}, biburl = {https://www.bibsonomy.org/bibtex/29dfbf99c842ef09e0f891349b8e4a90d/msn}, description = {SpringerLink - Journal Article}, file = {tsai00formal.pdf:papers\\ansoft\\tsai00formal.pdf:PDF}, interhash = {6c436bc9504a7e3c624994f8ec608108}, intrahash = {9dfbf99c842ef09e0f891349b8e4a90d}, journal = {Annals of Software Engineering}, keywords = {research.cs.softeng info.refs.journals.ansoft research.cs.softeng.formal}, month = {#nov#}, number = 1, pages = {207--223}, timestamp = {2009-06-25T16:50:50.000+0200}, title = {A comparative study of formal verification techniques for software architecture specifications}, url = {http://dx.doi.org/10.1023/A:1018960305057}, volume = 10, year = 2000 }