TY - GEN
T1 - A formal architecture pattern for real-time distributed systems
AU - Al-Nayeem, Abdullah
AU - Sun, Mu
AU - Qiu, Xiaokang
AU - Sha, Lui
AU - Miller, Steven P.
AU - Cofer, Darren D.
PY - 2009
Y1 - 2009
N2 - Pattern solutions [1] for software and architectures have significantly reduced design, verification, and validation times by mapping challenging problems into a solved generic problem. In the paper, we present an architecture pattern for ensuring synchronous computation semantics using the PALS protocol [2]. We develop a modeling framework in AADL to automatically transform a synchronous design of a real-time distributed system into an asynchronous design satisfying the PALS protocol. We present a detailed example of how the PALS transformation works for a dual-redundant system. From the example, we also describe the general transformation in terms of intuitively defined AADL semantics. Furthermore, we develop a static analysis checker to find necessary conditions that must be satisfied in order for the PALS transformation to work correctly. The transformations and static checks that we have described are implemented in OSATE using the generated EMF metamodel API for model manipulation.
AB - Pattern solutions [1] for software and architectures have significantly reduced design, verification, and validation times by mapping challenging problems into a solved generic problem. In the paper, we present an architecture pattern for ensuring synchronous computation semantics using the PALS protocol [2]. We develop a modeling framework in AADL to automatically transform a synchronous design of a real-time distributed system into an asynchronous design satisfying the PALS protocol. We present a detailed example of how the PALS transformation works for a dual-redundant system. From the example, we also describe the general transformation in terms of intuitively defined AADL semantics. Furthermore, we develop a static analysis checker to find necessary conditions that must be satisfied in order for the PALS transformation to work correctly. The transformations and static checks that we have described are implemented in OSATE using the generated EMF metamodel API for model manipulation.
KW - Architecture description language
KW - Architecture pattern
KW - Formal verification
KW - GALS
KW - Logical synchronization
UR - http://www.scopus.com/inward/record.url?scp=77649314785&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=77649314785&partnerID=8YFLogxK
U2 - 10.1109/RTSS.2009.50
DO - 10.1109/RTSS.2009.50
M3 - Conference contribution
AN - SCOPUS:77649314785
SN - 9780769538754
T3 - Proceedings - Real-Time Systems Symposium
SP - 161
EP - 170
BT - Proceedings - Real-Time Systems Symposium, RTSS 2009
T2 - Real-Time Systems Symposium, RTSS 2009
Y2 - 1 December 2009 through 4 December 2009
ER -