Proceedings International Workshop on Formal Engineering approaches to Software Components and Architectures

These are the proceedings of the 14th International Workshop on Formal Engineering approaches to Software Components and Architectures (FESCA). The workshop was held on April 22, 2017 in Uppsala (Sweden) as a satellite event to the European Joint Conference on Theory and Practice of Software (ETAPS'17). The aim of the FESCA workshop is to bring together junior researchers from formal methods, software engineering, and industry interested in the development and application of formal modelling approaches as well as associated analysis and reasoning techniques with practical benefits for software engineering. In recent years, the growing importance of functional correctness and the increased relevance of system quality properties (e.g. performance, reliability, security) have stimulated the emergence of analytical and modelling techniques for the design and development of software systems. With the increasing complexity and utilization of today's software systems, FESCA aims at addressing two research questions: (1) what role is played by the software design phase in the systematic addressing of the analytical and modelling challenges, and (2) how can formal and semi-formal techniques be effectively applied to make the issues easier to address automatically, with lower human intervention.


Similar Publications

An engineering design process may involve software modules that can executed concurrently. Concurrent modules can be very easily subject to some synchronization errors. This paper discusses verification process for such engineering software. Read More


We report an investigation of data analysis methods derived from other disciplines, which we applied to physics software systems. They concern the analysis of inequality, trend analysis and the analysis of diversity. The analysis of inequality exploits statistical methods originating from econometrics; trend analysis is typical of economics and environmental sciences; the analysis of diversity is based on concepts derived from ecology and treats software as an ecosystem. Read More


We report a methodology developed to quantitatively assess the maintainability of Geant4 with respect to software engineering references. The level of maintainability is determined by combining a set of metrics values whose references are documented in literature. Read More


In this paper, we introduce an interactive simulator for programs in the form of LLVM bitcode. The main features of the simulator include precise control over thread scheduling, automatic checkpoints and reverse stepping, support for source-level information about functions and variables in C and C++ programs and structured heap visualisation. Additionally, the simulator is compatible with DiVM (DIVINE VM) hypercalls, which makes it possible to load, simulate and analyse counterexamples from an existing model checker. Read More


Many modern parallel computing systems are heterogeneous at their node level. Such nodes may comprise general purpose CPUs and accelerators (such as, GPU, or Intel Xeon Phi) that provide high performance with suitable energy-consumption characteristics. However, exploiting the available performance of heterogeneous architectures may be challenging. Read More


The DICE workshop explores the area of Implicit Computational Complexity (ICC), which grew out from several proposals to use logic and formal methods to provide languages for complexity-bounded computation (e.g. Ptime, Logspace computation). Read More


In this paper we report the experience of using AutoProof to statically verify a small object oriented program. We identified the problems that emerged by this activity and we classified them according to their nature. In particular, we distinguish between tool-related and methodology-related issues, and propose necessary changes to simplify both tool and method. Read More


A number of formal methods exist for capturing stimulus-response requirements in a declarative form. Someone yet needs to translate the resulting declarative statements into imperative programs. The present article describes a method for specification and verification of stimulus-response requirements in the form of imperative program routines with conditionals and assertions. Read More


Over the past three decades, considerable effort has been devoted to the study of software architecture. A major portion of this effort has focused on the originally proposed view of four "C"s---components, connectors, configurations, and constraints---that are the building blocks of a system's architecture. Despite being simple and appealing, this view has proven to be incomplete and has required further elaboration. Read More


The next release problem (NRP) aims to effectively select software requirements in order to acquire maximum customer profits. As an NP-hard problem in software requirement engineering, NRP lacks efficient approximate algorithms for large scale instances. The backbone is a new tool for tackling large scale NP-hard problems in recent years. Read More