The microservices architectural style improves flexi-bility and performance but might come at the cost of complexity and cognitive effort. Understanding how architectural design decision affects cognitive effort can support software engineers in designing and building more maintainable systems. However, little research exists measuring the impact of architectural styles on developers' cognitive processes. To the best of our knowledge, no empirical study on navigation and comprehension strategies compares a microservice-based and monolithic variant of a trading system, which is widely used for empirical research on information system evolution. To assess the cognitive processes, we conducted an eye-tracking study (n=42) of typical maintenance tasks. We randomly assigned participants to two groups performing a feature location and a code change task using the trading system's monolithic or microservices-based implementation. Efficacy is significantly higher in the monolith variant. We investigate the reasons and propose a cognitively-grounded method to analyse comprehension strategies and estimate maintenance effort. We measure differences in comprehension strategies (top-down and bottom-up comprehension) and conclude that 1) there is a significant difference in visual effort and time taken to identify a specific feature, and 2) bottom-up comprehension is more frequently applied in microservices than in the monolith variant. Finally, we discuss our findings and their implications for practitioners and the research community.

Abstract State Machine (ASM) theory is a well-known state-based formal method to analyze and specify software and hardware systems. As in other state-based formal methods, the proposed modeling languages for ASMs still lack easy-to-comprehend abstractions to structure state and behavior aspects of specifications. Modern object-oriented languages offer a variety of advanced language constructs, and most of them either offer interfaces, mixins, or traits in addition to classes and inheritance. Our goal is to investigate these language constructs in the context of state-based formal methods using ASMs as a representative of this kind of formal methods. We report on a controlled experiment with 105 participants to study the understandability of the three language constructs in the context of ASMs. Our hypotheses are influenced by the debate of object-oriented communities. We hypothesized that the understandability (measured by correctness and duration variables) shows significantly better understanding for interfaces and traits compared to mixins, as well as at least a similar or better understanding for traits compared to interfaces. The results indicate that understandability of interfaces and traits show a similar good understanding, whereas mixins shows a poorer understanding. We found a significant difference for the correctness of understanding comparing interfaces with mixins.

Abstract State Machine (ASM) theory is a well-known state-based formal method. As in other state-based formal methods, the proposed specification languages for ASMs still lack easy-to-comprehend abstractions to express structural and behavioral aspects of specifications. Our goal is to investigate object-oriented abstractions such as interfaces and traits for ASM-based specification languages. We report on a controlled experiment with 98 participants to study the specification efficiency and effectiveness in which participants needed to comprehend an informal specification as problem (stimulus) in form of a textual description and express a corresponding solution in form of a textual ASM specification using either interface or trait syntax extensions. The study was carried out with a completely randomized design and one alternative (interface or trait) per experimental group. The results indicate that specification effectiveness of the traits experiment group shows a better performance compared to the interfaces experiment group, but specification efficiency shows no statistically significant differences. To the best of our knowledge, this is the first empirical study studying the specification effectiveness and efficiency of object-oriented abstractions in the context of formal methods.

In this paper we present CASM, a language based on Abstract State Machines (ASM), and its optimizing compiler. ASM is a well-defined (formal) method based on algebraic concepts. A distinct feature of ASM is its combination of parallel and sequential execution semantics. This makes it an excellent choice to formally specify and verify micro-architectures. We present a compilation scheme and an implementation of a runtime system supporting efficient execution of ASM.