Sokolsky, OlegLee, InsupClark, Duncan2023-05-222023-05-222006-04-292007-03-14https://repository.upenn.edu/handle/20.500.14332/6354The paper discusses the use of formal methods for the analysis of architectural models expressed in the modeling language AADL. AADL describes the system as a collection of interacting components. The AADL standard prescribes semantics for the thread components and rules of interaction between threads and other components in the system. We present a semantics-preserving translation of AADL models into the real-time process algebra ACSR, allowing us to perform schedulability analysis of AADL models.Presentation