We propose a definition of a class of reflective Abstract State Machines (ASMs) that extends the class of Parallel Guarded Assignments (PGAs), a subclass of single-agent sequential ASMs, and can serve as ground model for refinements of reflectivity in concrete programming languages.

We present Executable Abstract Programs and analyse their role for software development and documentation. The intuitive understanding of these programs fits the computational mindset of software system engineers and is supported by a simple but precise behavioural definition. Therefore, they can be smoothly integrated in the practitioner's daily work to rigorously formulate every design and implementation decision taken on the path from the Executable Abstract Program for the requirements to the targeted and efficiently runnable code. The Executable Abstract Programs of the resulting system documentation represent definitions of implementation steps one can check and justify by testing (due to their executable character) or by reasoning (due to the mathematical definition of their behaviour). For complex systems the implementation involves multiple (orthogonal or successive) implementation steps which represent instances of a practical computational refinement concept. Such a system development process is driven by computational refinements and is strictly limited to explicitly formulate and justify -- besides the requirements -- only the necessary implementation steps. As a consequence, it produces as side-effect a corpus of documentation that facilitates the understandability of the final code and improves its reliability and resilience; it also enhances the maintenance process (including reuse and change of abstract programs and code) and reduces maintenance cost.

To overcome the practical limitations of partial-order runs of ‘distributed ASMs’ (Abstract State Machines) proposed by Gurevich, we have defined a concept of concurrent runs of multi-agent ASMs and could show that concurrent ASMs capture a natural language-independent axiomatic definition of concurrent algorithms, thus generalising Gurevich’s seminal ‘Sequential ASM Thesis’ from sequential to concurrent algorithms. However, we remained intrigued by the fact that Blass and Gurevich used partial-order runs of distributed ASMs to explain runs of sequential recursive algorithms. We discovered that also the inverse simulation holds: for every distributed ASM with partial order runs, these runs can be described by runs of a sequential recursive algorithm. This surprising result clarifies the difference in expressivity between partial-order and concurrent runs.

Any concurrent system can be captured by a concurrent Abstract State Machine (cASM). This remains valid, if different agents can only interact via messages. It even permits a strict separation between memory managing agents and other agents that can only access the shared memory by sending query and update requests. This paper is dedicated to an investigation of replicated data that is maintained by a memory management subsystem, where the replication neither appears in the requests nor in the corresponding answers. We specify the behaviour of a concurrent system with such memory management using concurrent communicating ASMs (ccASMs), provide several refinements addressing different replication policies and internal messaging between data centres, and analyse their effects on the runs with respect to consistency. We show that on a concrete level even a weak form of consistency is only possible, if view serialisability can be guaranteed.

The development of code for software intensive systems involves numerous levels of abstraction, leading from requirements to code. Having abstract modeling concepts available as high-level programming constructs helps to define the code and to make sure that when the system runs with the software executed by machines, the software components behave in the expected way. We explain in this paper that nevertheless, there remains a gap, which cannot be closed by mere programming methods, but which can be closed if programming is supported by an appropriate modeling framework (a design and analysis method and a language).