View Item 
      •   Home
      • 1. Schools
      • College of Engineering
      • School of Computer Science and Engineering (SCSE)
      • SCSE Conference Papers
      • View Item
      •   Home
      • 1. Schools
      • College of Engineering
      • School of Computer Science and Engineering (SCSE)
      • SCSE Conference Papers
      • View Item
      JavaScript is disabled for your browser. Some features of this site may not work without it.
      Subject Lookup

      Browse

      All of DR-NTUCommunities & CollectionsTitlesAuthorsBy DateSubjectsThis CollectionTitlesAuthorsBy DateSubjects

      My Account

      Login

      Statistics

      Most Popular ItemsStatistics by CountryMost Popular Authors

      About DR-NTU

      Model checking software architecture design

      Thumbnail
      Author
      Zhang, Jiexin
      Liu, Yang
      Sun, Jing
      Dong, Jin Song
      Sun, Jun
      Date of Issue
      2012
      Conference Name
      IEEE International Symposium on High-Assurance Systems Engineering (14th : 2012 : Omaha, Nebraska, USA)
      School
      School of Computer Engineering
      Abstract
      Software Architecture plays an essential role in the high level description of a system design. Despite its importance in the software engineering practice, the lack of formal description and verification support hinders the development of quality architectural models. In this paper, we present an automated approach to the modeling and verification of software architecture designs using the Process Analysis Toolkit (PAT). We present the formal syntax of the Wright# architecture description language together with its operational semantics in Labeled Transition System (LTS). A dedicated model checking module for Wright# is implemented in the PAT verification framework based on the proposed formalism. The module - ADL supports verification and simulation of software architecture models in PAT. We advance our work via defining an architecture style library that embodies commonly used architecture patterns to facilitate the modeling process. Finally, a case study of the Teleservices and Remote Medical Care System (TRMCS) modeling and verification is presented to evaluate the effectiveness and scalability of our approach.
      Subject
      DRNTU::Engineering::Computer science and engineering
      Type
      Conference Paper
      Collections
      • SCSE Conference Papers
      http://dx.doi.org/10.1109/HASE.2012.12
      Get published version (via Digital Object Identifier)

      Show full item record


      NTU Library, Nanyang Avenue, Singapore 639798 © 2011 Nanyang Technological University. All rights reserved.
      DSpace software copyright © 2002-2015  DuraSpace
      Contact Us | Send Feedback
      Share |    
      Theme by 
      Atmire NV
       

       


      NTU Library, Nanyang Avenue, Singapore 639798 © 2011 Nanyang Technological University. All rights reserved.
      DSpace software copyright © 2002-2015  DuraSpace
      Contact Us | Send Feedback
      Share |    
      Theme by 
      Atmire NV
       

       

      DCSIMG