It is a long standing challenge to devise a formal model of ACT-R as a basis for formal reasoning on ACT-R. The ACT-R architecture is a composition of components (such as modules) with predefined interfaces between components and predefined interactions on the interfaces. Reasoning over the correctness of a formal model of ACT-R benefits from the separation of abstraction levels i.e. reasoning on the level of interfaces and interactions between components in isolation from the concrete behaviour of each component. We propose a formal semantics of ACT-R that preserves the structural properties of architectural components, i.e., the interfaces of modules to the remaining architecture as well as communication between modules within the architecture. We demonstrate how our new formal semantics of ACT-R serves to prove the correctness of the timed automaton based operational semantics for ACT-R (TA-ACT-R) on the level of architectural components.

Subject of this article is the question whether the potential forautomatic defect analysis for symbolic timed ACT-R models asdemonstrated in earlier work can be developed into a scalable andcomprehensible technique. We present a formal, operational modelof an ACT-R architecture and a translation scheme of ACT-Rmodels into timed automata. We have applied this translationto ACT-R models and report on scalability experiments withautomatic defect analysis.