Abstract State Machine

I spent several days to study Abstract State Machine (ASM) in depth. ASM is used to model BPEL as I mentioned in my survey paper on modeling Web service processes (not available online) and it is used for choreography with WSMO .

A state in an ASM is not just a label as in Finite State Machine (FSM), but contains arbitrary data structures. The rules are associated with transition rules (guards). These rules can be triggered simultaneously when a state satisfies the guards, which makes ASM a nature machine for concurrency (also called synchronous parallelism). A run of ASM is a (finite or infinite) sequence of states. Up to here, ASM is similar to tie (an extension of Petri nets).

ASM is a further development of the notion of “evolving algebra” first introduced by Gurevich. ASM thesis is proved to strength the Church-Turing thesis. With more convenient way to model software, ASM is widely used as a rigorous method for the design and analysis of large software systems. For example, ASM can model the major software life cycle activities: requirements capture (by ground model), architecture and component design (via stepwise refined model), validation (by simulation), verification (by proof techniques), documentation (by recording all the intermediate models and design decisions).

ASM can also used for modeling distributed behaviours.