ABS

ABS Tools and Methods

ABS is a language for Abstract Behavioral Specification of distributed and concurrent systems, which supports the modelling of resource restrictions and resource management. It combines implementation-level specifications with verifiability, high-level design with executability, and formal semantics with practical usability. ABS is a concurrent, object-oriented, modelling language that features functional data types. It is designed to develop executable models with a parallel, object-oriented program flow and targets distributed and concurrent systems by means of concurrent object groups and asynchronous method calls. The time model of ABS enables modeling of time-aware, discrete event simulation scenarios. Model variability support is based on feature models and delta-oriented specifications.  Deployment modelling can be based on high-level deployment models. The ABS system supports the modelling of resource-aware and resource-restricted systems and provides a range of techniques for model exploration and analysis, based on formal semantics. ABS models can react to external stimuli and make simulation state and results available as structured JSON data.

This webpage contains only abstract information. For detailed information on methodology and applications, please visit the ABS homepage https://abs-models.org

Challenges

Sirius is cooperating with HVL Bergen in multiple case studies to model workflows in the healthcare domain using ABS, particularly but not only in the pathology department. The case studies are done in cooperation with Helse Vest (HNV).

UiO is developing Crowbar, a deductive verification tool for ABS using symbolic execution.  This will enable users of ABS to prove the correctness of ABS models.

Our Approach

The following major features were added to ABS with the support of SIRIUS:

  • ABS now can record and replay simulation runs. This is important to exactly reproduce a specific simulation run. (Lars Tveito)
  • SQLite databases can now be accessed (read-only) from within a running ABS model. This enables data-driven models, or models that can be parameterized by a domain expert instead of an expert in the ABS language itself.  Note that many other structured data formats (CSV, Excel) can easily be converted into SQLite.  (Rudolf Schlatte)
  • ABS models can now include model-specific visualizations. The user can connect a web browser to a running ABS model and see current or final states of a simulation.  This was used, e.g., in the Planning and Logistics case study to visualize timelines of vessel traffic and container movements.  (Rudolf Schlatte)
  • A separate tool, Crowbar, implements a symbolic execution engine for ABS based on BPL (Behavioral Program Logic). (Eduard Kamburjan et al.)
  • The support by Sirius also made many smaller additions to the language and general maintenance possible.

Results

ABS is an open-source research project.

Documentation

Language documentation, examples and tutorials are on the ABS homepage at https://abs-models.org

Source Code

Source code is available at [GitHub]

Publications

Einar Broch Johnsen, Reiner Hähnle, Jan Schäfer, Rudolf Schlatte, Martin Steffen:ABS: A Core Language for Abstract Behavioral Specification. FMCO 2010: 142-164

Rudolf Schlatte, Einar Broch Johnsen, Eduard Kamburjan, Silvia Lizeth Tapia Tarifa:Modeling and Analyzing Resource-Sensitive Actors: A Tutorial Introduction.COORDINATION 2021: 3-19

Elvira Albert, Frank S. de Boer, Reiner Hähnle, Einar Broch Johnsen, Rudolf Schlatte, Silvia Lizeth Tapia Tarifa, Peter Y. H. Wong:Formal modeling and analysis of resource management for cloud architectures: an industrial case study using Real-Time ABS. Serv. Oriented Comput. Appl. 8(4): 323-339 (2014)

Rudolf Schlatte; Einar Broch Johnsen; Eduard Kamburjan; S. Lizeth Tapia Tarifa: The ABS simulator toolchain. Science of Computer Programming 2022-11 | Journal article DOI: 10.1016/j.scico.2022.102861

Team

SIRIUS:

Rudolf Schlatte, Lars Tveito, Eduard Kamburjan, Einar Broch Johnsen, Silvia Lizeth Tapia Tarifa, et al.

Partners

Acknowledgements

This work was partially supported by the SIRIUS Centre for Scalable Data Access (Research Council of Norway, project 237889).

The development of the ABS language and tools has been supported by a number of European FP7 and H2020 research projects.

  • HATS: Highly Adaptive and Trustworthy Software using Formal Methods
  • Envisage: Engineering Virtualized Services
  • HyVar: Scalable Hybrid Variability