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

Case Studies

  • E. Albert, F. de Boer, R. Hähnle, E. B. Johnsen, R. Schlatte, S. L. Tapia Tarifa, 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.
  • J-C Lin, I. C. Yu, E. B. Johnsen, M-C Lee. ABS-YARN: A Formal Framework for Modeling Hadoop YARN Clusters.
    Proc. 19th Intl. Conf. on Fundamental Approaches to Software Engineering  (FASE 2016). LNCS 9633. Springer, 2016.
    DOI: 10.1007/978-3-662-49665-7_4. Download a preprint.

Language Development

  • 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.

Deductive Verification

  • 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. 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.

Cost Analysis

  • 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.

Deadlock Analysis

  • E. Giachino, C. Laneve, and M. Lienhardt.
    A Framework for Deadlock Detection in ABS.
    Journal of Software and Systems Modeling, to appear, 2015.
    DOI: 10.1007/s10270-014-0444-y. Download a preprint.

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.
    Resource-aware applications for the cloud.
    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.