% % GENERATED FROM http://acme.able.cs.cmu.edu % by : anonymous % IP : ec2-54-90-167-73.compute-1.amazonaws.com % at : Fri, 29 Mar 2024 05:14:46 -0400 GMT % % Selection : Author: Jung-Soo_Kim % @InProceedings{Kim2006, AUTHOR = {Kim, Jung Soo and Garlan, David}, TITLE = {Analyzing Architectural Styles with Alloy}, YEAR = {2006}, MONTH = {17 July}, BOOKTITLE = {Workshop on the Role of Software Architecture for Testing and Analysis 2006 (ROSATEA 2006)}, ADDRESS = {Portland, ME, USA}, PDF = {http://acme.able.cs.cmu.edu/pubs/uploads/pdf/rosatea2006-final.pdf}, ABSTRACT = {The backbone of many architectures is an architectural style that provides a domain-specific design vocabulary and set of constraints on how that vocabulary can be used. Hence, designing a sound and appropriate architectural style becomes an important and intellectually challenging activity. Unfortunately, although there are numerous tools to help in the analysis of individual architectures, relatively less work has been done on tools to help the style designer. In this paper we show how to map an architectural style, expressed formally in an architectural description language, into a relational model that can be automatically checked for properties such as whether a style is consistent, whether a style satisfies some predicate over the architectural structure, whether two styles are compatible for composition, and whether one style refines another.}, KEYWORDS = {Acme, Formal Methods, Software Architecture} } @InProceedings{Kim2003, AUTHOR = {Garlan, David and Khersonsky, Serge and Kim, Jung Soo}, TITLE = {Model Checking Publish-Subscribe Systems}, YEAR = {2003}, MONTH = {May}, BOOKTITLE = {Proceedings of The 10th International SPIN Workshop on Model Checking of Software (SPIN 03)}, ADDRESS = {Portland, OR}, PDF = {http://www.cs.cmu.edu/afs/cs/project/able/ftp/SPIN03/SPIN03.pdf}, ABSTRACT = {While publish-subscribe systems have good engineering properties, they are difficult to reason about and to test. Model checking such systems is an attractive alternative. However, in practice coming up with an appropriate state model for a pub-sub system can be a difficult and error-prone task. In this paper we address this problem by describing a generic pub-sub model checking framework. The key feature of this framework is a reusable, parameterized state machine model that captures pub-sub runtime event management and dispatch policy. Generation of models for specific pub-sub systems is then handled by a translation tool that accepts as input a set of pub-sub component descriptions together with a set of pub-sub properties, and maps them into the framework where they can be checked using off-the-shelf model checking tools.}, KEYWORDS = {Model Checking, Publish Subscribe Systems} } @Article{Kim2010, AUTHOR = {Kim, Jung Soo and Garlan, David}, TITLE = {Analyzing Architectural Styles}, YEAR = {2010}, JOURNAL = {Journal of Software and Systems}, VOLUME = {83}, NUMBER = {7}, PAGES = {1216-1235}, PDF = {http://acme.able.cs.cmu.edu/pubs/uploads/pdf/JSS-final-revision3.pdf}, ABSTRACT = {The backbone of most software architectures and component integration frameworks is one or more architectural styles that provide a domain-speci c design vocabulary and a set of constraints on how that vocabulary is used. Today's architectural styles are increasingly complex, involving rich vocabularies and numerous constraints. Hence, designing a sound and appropriate style becomes an intellectually challenging activity. Unfortunately, although there are numerous tools to help in the analysis of architectures for individual systems, relatively less work has been done on tools to help in the design of architectural styles. In this paper we address this gap by showing how to map an architectural style, expressed formally in an architectural description language, into a relational model that can then be checked for properties, such as whether a style is consistent, whether a style satis es some predicates over its architectural structure, and whether two styles are compatible for composition.}, KEYWORDS = {Architectural Analysis, Architectural Style} }