Publications and workshops

This page lists ABS workshops and selected research papers on the development and usage of the ABS modeling language and analysis tools.

ABS workshops

Case studies

  • G. Turin, A. Borgarelli, S. Donetti, F. Damiani, E. B. Johnsen, and S. L. Tapia Tarifa.
    Predicting resource consumption of Kubernetes container systems using resource models
    Journal of Systems and Software, Volume 203, September 2023.
    DOI: 10.1016/j.jss.2023.111750. Download a preprint.
  • J-C Lin, M-C Lee, I. C. Yu, and E. B. Johnsen.
    A configurable and executable model of Spark Streaming on Apache YARN
    International Journal of Grid and Utility Computing. Volume 11(2). Indescience, 2020.
    DOI: 10.1504/IJGUC.2020.105531. Download a preprint.
  • E. Kamburjan, R. Hähnle, and S. Schön
    Formal modeling and analysis of railway operations with active objects
    Science of Computer Programming. Volume 166. Elsevier, 2018.
    DOI: 10.1016/j.scico.2018.07.001.
  • E. Albert, F. de Boer, R. Hähnle, E. B. Johnsen, R. Schlatte, S. L. Tapia Tarifa, and P. Y. H. Wong.
    Formal modeling and analysis of resource management for cloud architectures: an industrial case study using Real-Time ABS
    Service Oriented Computing and Applications 8 (4):323-339, 2014.
    DOI: 10.1007/s11761-013-0148-0. Download a preprint.

Language development

  • L. Tveito, E. B. Johnsen, and R. Schlatte.
    Global Reproducibility through Local Control for Distributed Active Objects
    In Proc. 23th International Conference on Fundamental Approaches to Software Engineering (FASE 2020), LNCS 12076. Springer , 2020.
    DOI: 10.1007/978-3-030-45234-6_7. Download a preprint.
  • R. Schlatte, E. B. Johnsen, J. Mauro, S. L. Tapia Tarifa, and I. C. Yu.
    Release the Beasts: When Formal Methods Meet Real World Data
    Festschrift Farhad Arbab, LNCS 10865. Springer , 2018.
    DOI: 10.1007/978-3-642-25271-6_8. Download a preprint.
  • E. Kamburjan.
    From post-conditions to post-region invariants: deductive verification of hybrid objects
    In 24th ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2021). ACM , 2021.
    DOI: 10.1145/3447928.3456633.
  • E. B. Johnsen, R. Hähnle, J. Schäfer, R. Schlatte, and M. Steffen.
    ABS: A Core Language for Abstract Behavioral Specification
    In Proc. 9th Intl. Symp. on Formal Methods for Components and Objects (FMCO 2010), LNCS 6957. Springer , 2011.
    DOI: 10.1007/978-3-642-25271-6_8. Download a preprint.
  • E. B. Johnsen, R. Schlatte, and S. L. Tapia Tarifa.
    Integrating Deployment Architecture and Resource Consumption in Timed Object-Oriented Models
    Journal of Logical and Algebraic Methods in Programming 84(1): 67-91, 2015.
    DOI: 10.1016/j.jlamp.2014.07.001. Download a preprint.
  • Joakim Bjørk, Frank S. de Boer, Einar Broch Johnsen, Rudolf Schlatte, and S. L. Tapia Tarifa.
    User-defined schedulers for real-time concurrent objects
    Innovations Syst Softw Eng 9(1): 29-43 (2013).
    DOI: 10.1007/s11334-012-0184-5. Download a preprint.
  • F. Damiani, R. Hähnle, E. Kamburjan, M. Lienhardt.
    A Unified and Formal Programming Model for Deltas and Traits
    Proc. 20th International Conference on Fundamental Approaches to Software Engineering (FASE 2017), LNCS 10202. Springer, 2017.
    DOI: 10.1007/978-3-662-54494-5_25. Download a [postprint <http://hdl.handle.net/2318/1633390>`__.

Software product lines

  • F. Damiani, R. Hähnle, E. Kamburjan, M. Lienhardt, and L. Paolini.
    Variability modules
    Journal of Systems and Software, Volume 195, January 2023.
    DOI: 10.1016/j.jss.2022.111510.
  • F. Damiani, M. Lienhardt, R. Muschevici, I. Schaefer.
    An Extension of the ABS Toolchain with a Mechanism for Type Checking SPLs
    Proc. 13th International Conference on Integrated Formal Methods (IFM 2017), LNCS 10510. Springer, 2017.
    DOI: 10.1007/978-3-319-66845-1_8. Download a [postprint <http://hdl.handle.net/2318/1649744>`__.

Deductive verification

  • E. Kamburjan, C. C. Din, R. Hähnle and E. B. Johnsen.
    Behavioral Contracts for Cooperative Scheduling
    In Deductive Software Verification: Future Perspectives, LNCS 12345. Springer, 2020.
    DOI: 10.1007/978-3-030-64354-6_4. Download a preprint.
  • C. C. Din, R. Bubel and R. Hähnle.
    KeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABS
    In Proc. 25th Intl. Conf. on Automated Deduction (CADE 2015), LNCS 9195. Springer, 2015.
    DOI:[10.1007/978-3-319-21401-6_35 <http://doi.org/10.1007/978-3-319-21401-6_35>`__. Download a preprint.
  • C. C. Din, S. L. Tapia Tarifa, R. Hähnle and E. B. Johnsen.
    History-Based Specification and Verification of Scalable Concurrent and Distributed Systems
    In Proc. 17th Intl. Conf. on Formal Engineering Method (ICFEM 2015), LNCS 9407. Springer, 2015.
    DOI: 10.1007/978-3-319-25423-4_14. Download a preprint.

Analysis

  • C. Laneve, M. Lienhardt, K. I Pun, and G. Román-Díez.
    Time analysis of actor programs
    Journal of Logical and Algebraic Methods in Programming, Volume 105, Elsevier, 2019.
    DOI: 10.1016/j.jlamp.2019.02.007.
  • A. Garcia, C. Laneve, and M. Lienhardt.
    Static analysis of cloud elasticity
    Science of Computer Programming, Volume 147, Elsevier, 2017.
    DOI: 10.1016/j.scico.2017.03.008.
  • E. Albert, P. Arenas, A. Flores-Montoya, S. Genaim, M. Gómez-Zamalloa, E. Martin-Martin, G. Puebla, and G. Román-Díez.
    SACO: Static Analyzer for Concurrent Objects
    In Proc. 20th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS 8413, Springer, 2014.
    DOI: 10.1007/978-3-642-54862-8_46. Download a preprint.
  • E. Giachino, C. Laneve, and M. Lienhardt.
    A Framework for Deadlock Detection in ABS
    Journal of Software and Systems Modeling, Volume 15(4), Springer, 2015.
    DOI: 10.1007/s10270-014-0444-y.

ABS tools

  • Rudolf Schlatte, Einar Broch Johnsen, Eduard Kamburjan and S. Lizeth Tapia Tarifa
    The ABS simulator toolchain
    Science of Computer Programming. Volume 233. Elsevier, 2022.
    DOI: 10.1016/j.scico.2022.102861.

Code generation from ABS

  • B. Nobakht and F. S. de Boer.
    Programming with Actors in Java 8
    In Proc. of the 6th Intl. Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA’14). LNCS 8803. Springer, 2014.
    DOI: 10.1007/978-3-662-45231-8_4. Download a preprint.

Model-based deployment and monitoring

  • R. Hähnle and E. B. Johnsen.
    Designing Resource-Aware Cloud Applications
    IEEE Computer 48 (6), 2015.
    DOI: 10.1109/MC.2015.172. Download a preprint.
  • B. Nobakht, S. de Gouw and F.S. de Boer.
    Formal Verification of Service Level Agreements Through Distributed Monitoring
    In Proc. 4th European Conf. on Service Oriented and Cloud Computing (ESOCC 2015). LNCS 9306, Springer, 2015.
    DOI: 10.1007/978-3-319-24072-5_9. Download a preprint.