ASYDE 2020

15th September Amsterdam, The Netherlands - Virtual Event
2nd International Workshop on Automated and verifiable Software sYstem DEvelopment
Co-located with the 18th International Conference on Software Engineering and Formal Methods (SEFM 2020)

ASYDE Workshop Recording

Recent News

Because of the COVID-19 pandemic, following the decision taken by the SEFM 2020 organisers, also ASYDE 2020 will not take place physically but will be replaced by a virtual event. As usual, ASYDE 2020 accepted contributions will be included in the LNCS post-proceedings and all accepted papers will have to be presented at the virtual conference in order to be included in the LNCS volume. How the virtual conference will be organised is still under consideration, e.g., live presentations and/or recorded ones.

Call for Papers

During the last three decades, automation in software development has gone mainstream. Software development teams strive to automate as much of the software development activities as possible. Automation helps, in fact, to reduce development time and cost, as well as to concentrate knowledge by bringing quality into every step of the development process.
Realizing high-quality software systems requires producing software that is efficient, error-free, cost-effective, and that satisfies customer requirements. Thus, one of the most crucial factors impacting software quality concerns not only the automation of the development process but also the ability to verify the outcomes of each process activity and the goodness of the resulting software product as well. Realizing high-quality software systems requires producing software that is efficient, error-free, cost-effective, and that satisfies evolving requirements. Thus, one the most crucial factors impacting software quality concerns not only the automation of the development process but also the ability to verify the outcomes of each process activity and the goodness of the resulting software product as well.
This becomes particularly true these days when we are, and will be, increasingly surrounded by a virtually infinite number of software artifacts - often underspecified - that can be composed to build new applications. This situation radically changes the way software will produced and used:

    - software is increasingly produced according to a certain goal, that can change during the system's execution, and by integrating existing software;
    - the focus of software production is then on the ability to perform automated reasoning to achieve software integration and development that can be kept always correct-by-construction via static and dynamic verification.


ASYDE 2020 provides a forum for researchers and practitioners to propose and discuss on automated software development methods and techniques, compositional verification theories, integration architectures, flexible and dynamic composition, and automated planning mechanisms.


ASYDE 2020 welcomes research papers, (industrial) experience papers and case-studies, tool demonstrations and visionary papers; nevertheless, papers describing novel research contributions and innovative applications are of particular interest.


Publication


Topics of interest include, but are not limited to, the following:

  • Specification, architecture, and design of software and verification models
  • Formal methods for automated software development
  • Model-driven software development
  • Correct-by-construction software development
  • Automated synthesis of software integration code
  • Automated software development and integration
  • Automated and verifiable software development
  • Automated planning methods
  • Description and validation of Non-functional properties of software
  • Software quality assurance for automated software development
  • Compositional theories for software development and its (dynamic) verification
  • Dynamic verification and testing
  • Service-oriented and Component-based software development
  • Machine learning techniques
  • Formal specification of (micro)services
  • Formal models for microservices
  • Automatic methods for the development and verification of smart contracts
  • Methods and tools for (semi)-automatically migrating monolithic systems to component-based or microservice-based systems

ASYDE bio

The ASYDE workshop wants to be the pooling of efforts we have been making over the past decade for organizing a number of successful workshops in the area of Software Engineering and Formal Methods.
It is a follow-up workshop bringing together the following previous events OrChor 2014, SCFI 2015, SCART 2015, VeryComp 2016.
The mission of the ASYDE workshop is to consolidate interest of the SEFM community and related forums on the interplay between software engineering and formal aspects of automated and verifiable software system development.
The steering committee will ensure continuity in the establishment and cross-fertilization of the ASYDE discussion forum towards continuous progress in this important research area.

Important Dates

Paper Submission

July 16th, 2020

July 31nd, 2020

Notification

August 10th, 2020

August 24th, 2020


Submission

ASYDE 2020 welcomes research papers (both long and short), experience reports and tool presentations; nevertheless, papers describing novel research contributions and innovative applications are of particular interest. Accepted papers will be included in the Springer LNCS post-proceedings of SEFM.
Contribution can be:

Regular papers (from 10 to 15 pages): in this category fall contributions that propose novel research work, address challenging problems with innovative ideas, or offer practical contributions (e.g., industrial experiences and case-studies) in the application of FM and SE approaches for building software systems via automated development and verification. Regular papers should clearly describe the situation or problem tackled, the relevant state of the art, the position or solution suggested and the potential benefits of the contribution. Authors of papers reporting industrial experiences are strongly encouraged to make their experimental results available for use by reviewers. Similarly, case-study papers should describe significant case-studies and the complete development should be made available for use by reviewers.

Short papers (from 6 to 8 pages): this category includes tool demonstrations, position papers, well-pondered and sufficiently documented visionary papers. Tool demonstration papers should explain enhancements made in comparison to previously published work. Authors of demonstration papers should make their tool available for use by reviewers.


All papers must:

    - be written in English;
    - be at least 10 pages long (regular papers) or 6 pages long (short papers);
    - not exceed 8 pages (short papers) or 15 pages (regular papers) for the submission and pre-proceedings (up to 2 additional pages will be given for the post-proceedings, only to address reviewers’ comments and feedback from the workshop)

Submissions are required to report on original, unpublished work and should not be submitted simultaneously for publication elsewhere (IFIP's Author Code of Conduct).

Each submitted paper will undergo a formal peer review process by at least 3 Program Committee members.

Paper submission is done via EasyChair.

Registration

Registration is now open. The virtual conference will be organised by live presentations (the program will be available soon), using Zoom. Participation is free, but registering to the mailing list is required in order to receive the Zoom link. Note that, once the registration to the mailing list is requested, it is necessary to confirm the registration by clicking on the link received on your e-mail.

Invited Speakers

Emilio Tuosto

Title

Open Problems in Choreographic Development of Message-Passing Applications - Presentation Available

Abstract

Communicating systems are ubiquitous and message-passing is gaining momentum as a suitable programming paradigm and coordination model. Design methods, tools, and programming approaches based on choreographies have attracted the attention of both academy and software industry. Important steps forward have been made thanks to the adoption of those techniques both in the realm of formal methods and for practical support to the engineering of message-passing software. Choreographies can be used at different stages of the development life-cycle of message-passing software. In fact, choreographies (i) are a suitable specification language, (ii) naturally enable model-driven development, and (iii) offer support to formal verification and to automatic code generation. Yet developing and reasoning about message-passing applications is difficult. After glossing over a few paradigmatic examples of techniques based on choreographies, this talk will highlight some of their limitations and discuss some open problems in choreographic development.

Info

Edward A. Lee

Title

More Deterministic Software for Cyber-Physical Systems - Presentation Available - Talk Recording

Abstract

The design of concurrent, real-time, and distributed software for embedded systems, robotics, and the internet of things has been evolving, moving away from low-level C code and RTOS scheduling. Increasingly promising frameworks based on publish-and-subscribe (e.g. ROS, MQTT), service-oriented architectures (e.g. gRPC, Apache Thrift), or actors (e.g. Erlang, Ray, Akka) offer higher-level abstractions with better control over concurrency. However, these technologies have been developed for or modeled after enterprise-scale information technology and have not been adapted to the unique requirements of cyber-physical systems. In particular, they have nondeterministic concurrency and weak control over timing. Moreover, these technologies are not well poised to take advantage of impending technology improvements in time-sensitive networking and precision-timed microprocessors.
In this talk, I will introduce Lingua Franca, a polyglot coordination language with an explicit model of time, more deterministic concurrency, and support for efficient, fault-tolerant, distributed applications. In Lingua Franca, components called reactors (actors revisited) execute under a deterministic, discrete-event model of computation that combines the best features of actors with the best features of synchronous languages. The functionality of a reactor is written in an unmodified target language (currently C, C++, or TypeScript). Using the C target, the Lingua Franca compiler generates extremely efficient, low footprint embedded C code that can execute on an embedded bare-iron platform or on a high-end multicore microprocessor, transparently exploiting application parallelism and realizing earliest-deadline-first scheduling. With the TypeScript target, seamless integration with the Node.js ecosystem offers a wealth of high-level IoT capabilities.
The Lingua Franca design team currently consists of Marten Lohstroh, Christian Menard, Soroush Bateni, Matt Weber, Alexander Schulz-Rosengarten, Shaokai Lin, and Edward Lee, with smaller contributions from a number of others. The language and implementation are open source with a BSD license. Many aspects of the language design are based on decades of experience with the Ptolemy II framework.

Info

Program

14:00 - 14:10

Opening

Federico Ciccozzi
Welcome message


Session 1 - Verification

Chair: Federico Ciccozzi

14.10 - 14:35

Presenter: Sneha Sahu

Model Translation from Papyrus-RT into the nuXmv Model Checker - Presentation Available

Virtual Room

14.35 - 15:00

Presenter: Maya Souilah

Modeling and Verification of Temporal Constraints for Web Service Composition - Presentation Available

Virtual Room


Invited Talk 1

Chair: Marjan Sirjani

15.00 - 15:45

More Deterministic Software for Cyber-Physical Systems - Presentation Available- Talk Recording

Edward A. Lee


15:45 - 16.00

Break



Session 2 - Security

Chair: Francesco Gallo

16.00 - 16:25

Presenter: Samri Ouchani

Modeling Attack-Defense Trees Countermeasures using Continuous Time Markov Chains - Presentation Available

Virtual Room


Invited Talk 2

Chair: Francesco Gallo

16.30 - 17:15

Open Problems in Choreographic Development of Message-Passing Applications - Presentation Available

Emilio Tuosto


Session 3 - Validation and Testing

Chair: Francesco Gallo

17.15 - 17:40

Presenter: Tim Soethout

Automated Validation of State-Based Client-Centric Isolation with TLA+ - Presentation Available

Virtual Room

17.40 - 18:05

Presenter: Krystof Sykora

Code Coverage Aware Test Generation Using Constraint Solver - Presentation Available

Virtual Room
Download Program

Program Committee

    Luciano Baresi - Politecnico di Milano, Italy
    Steffen Becker - University of Stuttgart, Germany
    Domenico Bianculli - University of Luxembourg, Luxembourg
    Antonio Brogi - Universita' di Pisa, Italy
    Giovanni Denaro - Universita' di Milano - Bicocca, Italy
    Antinisca Di Marco - Università dell'Aquila, Italy
    Amleto Di Salle - Università dell'Aquila, Italy
    Ehsan Khamespanah - University of Tehran, Iran
    Marina Mongiello - Politecnico di Bari, Italy
    Cristina Seceleanu - Mälardalen University, Sweden
    Meng Sun - Peking University, China
    Apostolos Zarras - University of Ioannina, Greece

Organizers and Main Contact

    Marco Autili (main contact)
    Department of Information Engineering, Computer Science and Mathematics - University of L’Aquila, L’Aquila (AQ), Italy
    email: marco.autili@univaq.it
    web-page: http://people.disim.univaq.it/marco.autili/
    Federico Ciccozzi
    Division of Computer Science and Software Engineering – Mälardalen University,
    Västerås, Sweden
    email: federico.ciccozzi@mdh.se
    web-page: : www.es.mdh.se/staff/266-Federico_Ciccozzi
    Francesco Gallo
    Department of Information Engineering, Computer Science and Mathematics - University of L’Aquila, L’Aquila (AQ), Italy
    email: francesco.gallo@univaq.it
    web-page: http://people.disim.univaq.it/francesco.gallo
    Marjan Sirjani
    Division of Computer Science and Software Engineering – Mälardalen University,
    Västerås, Sweden
    email: marjan.sirjani@mdh.se
    web-page: http://www.es.mdh.se/staff/3242-Marjan_Sirjani

Steering Committee

Farhad Arbab, Centre for Mathematics and Computer Science (The Netherlands)
Marco Autili, University of L’Aquila (Italy)
Federico Ciccozzi, Mälardalen University, (Sweden)
Dimitra Giannakopoulou, NASA (USA)
Pascal Poizat, LIP6 (France)
Massimo Tivoli, University of L’Aquila (Italy)

Web Chair

Francesco Gallo, University of L’Aquila (Italy)

Publicity Chair

Alexander Perucci, University of L’Aquila (Italy)

Venue

How To Get Here

CWI is located at Amsterdam Science Park, one of the largest concentrations in exact sciences in Europe. It is a hub for research, innovation and entrepreneurship and home of world class research institutes, universities and more than 130 companies, from science based start-ups to multinationals. With over 10,000 students, scientists and entrepreneurs, the park offers excellent opportunities for research and businesses. Amsterdam Science Park is a joint development by the University of Amsterdam, the City of Amsterdam and the Dutch Research Council (NWO).

By Car

CWI is located at Science Park 123, 1098 XG Amsterdam. The street name 'Science Park' has been in use since 2011 and might not be implemented in all navigation systems. In case your navigation system does not recognize 'Science Park 123', please use the old address ‘Kruislaan 413, 1098 SJ Amsterdam’ instead.

Directions

    Exit the A10 ringroad at S113/Watergraafsmeer
    Follow the Science Park signs; these will direct you to the Kruislaan
    Turn left onto the Carolina MacGillavrylaan after passing through the railroad tunnel
    Take the Science Park entry at your right and enter the gate

By Bus

Bus 40 serves Amsterdam Science Park four times an hour from stations Amsterdam Amstel (train, metro, tram) and Amsterdam Muiderpoort (train, tram). Get off at bus stop 'Science Park' or 'Science Park Aer'. During rush hour bus 240 can be used, too.

By Train

CWI is a five minute walk away from NS station Amsterdam Science Park. This station is served four times an hour from the directions Amsterdam Centraal – Schiphol and Almere – Amersfoort. Walk through the tunnel after leaving the platform for the science park (northeast exit), cross the street (Carolina MacGillavrylaan) at the crosswalk and walk past the brown building of Amsterdam University College. You will be able to see CWI’s main entrance on your left behind the parking lot.