Automated Extraction of Abstract Behavioural Models from JMS Applications

Distributed systems are hard to program, understand and analyze. Two key sources of complexity are the many possible behaviors of a system, arising from the parallel execution of its distributed nodes, and the handling of asynchronous messages exchanged between nodes. We show how to systematically construct executable models of publish/subscribe systems based on the Java Messaging Service (JMS). These models, written in the Abstract Behavioural Specification (ABS) language, capture the essentials of the messaging behavior of the original Java systems, and eliminate details not related to distribution and messages. We report on jms2abs, a tool that automatically extracts ABS models from the bytecode of JMS systems. Since the extracted models are formal and executable, they allow us to reason about the modeled JMS systems by means of tools built specifically for the modeling language. For example, we have succeeded to apply simulation, termination and resource analysis tools developed for ABS to, respectively, execute, prove termination and infer the resource consumption of the original JMS applications.