ForMABS 2016 – Proceedings

Message from the Chairs
We proposed the one-day workshop to ASE workshop chairs, primarily to identify like-minded researchers from academia and industry, working in the areas of formal methods and program analysis to meet and discuss issues pertaining to business systems and how formal methods can be applied to them. In the long run, our objective is to positively influence the design, development, evolution and transformation of real-life business systems with novel methods and techniques, especially based on formal methods and program analysis. These techniques have attained a significant level of sophistication today and can seamlessly scale to systems of non-trivial size and complexity. With this objective, we have organized the following key notes and invited talks for the workshop.

Invited Talks

Flexible, Adaptable, and Compliant Business Systems with Dynamic Condition Response Graphs
Thomas Hildebrandt
(IT University of Copenhagen, Denmark)
Software systems are increasingly used to support business processes and knowledge workflows within critical areas, including transportation, finance, healthcare and government. The support for such processes, which are at the same time unpredictable and subject to changing legal constraints, calls for flexibility, adaptability and compliancy. In this talk we will present theory and applications of Dynamic Condition Response (DCR) graphs, a formal declarative event-based process language implemented in the commercial web-tool DCRGraphs.net for collaborative process design and simulation and the academic tools dcr.itu.dk. The language and tools are the result of a series of research and PhD projects supported by the danish national research foundations, ITU and Exformatics A/S and the ongoing Computational Artefacts (CompArt.ku.dk) project supported by the Velux foundation.

SemFix and Beyond: Semantic Techniques for Program Repair
Abhik Roychoudhury
(National University of Singapore, Singapore)
Automated program repair is of great promise for future programming environments. It is also of obvious importance for patching vulnerabilities in software, or for building self-healing systems for critical infra-structure. Traditional program repair techniques tend to lift the fix from elsewhere in the program via syntax based approaches. In this talk, I will mention how the search problems in program repair can be solved by semantic analysis techniques. Here semantic analysis methods are not only used to guide the search, but also for extracting formal specifications from tests. I will conclude with positioning of the syntax based and semantic based methods for vulnerability patching, future generation programming, and self-healing systems.

Business Process Adaptation using Discrete Event Controller Synthesis
Sebastian Uchitel
(University of Buenos Aires, Argentina; Imperial College London, UK)
Discrete Event Controller Synthesis is a fully automated procedure for producing operational reactive strategies for achieving declarative goals. In this talk I will discuss how synthesis at runtime can play a key role in achieving self-adaptation. I will discuss a reference architecture for self-adaptive systems and focus on the problem of dynamic controller update. I will also explain why discrete event controller synthesis is particularly well suited for runtime adaptation of business processes, in particular for dynamic update of workflows.

Static Analysis to Enable Verification and Transformation of Data-Intensive Business Applications
Komondoor V. Raghavan
(Indian Institute of Science, India)
Programs that process data that reside in files are widely used in varied enterprise domains, such as banking, healthcare, and web-traffic analysis. Precise static analysis of these programs in the context of software transformation and verification tasks is a challenging problem. Our key insight is that static analysis of file- processing programs can be made more useful if knowledge of the input file formats of these programs is made available to the analysis. We instantiate this idea to solve two practical problems: specializing the code of a program to a given restricted input file format, and verifying if a program conforms to a given input file format. We then discuss an implementation of our approach, and also empirical results on a set of real and realistic programs. The results are very encouraging in the terms of both scalability as well as precision of the approach.

Full Papers

Improving Configurable Software Testing with Statistical Test Selection
Dusica Marijan
(Simula Research Laboratory, Norway)
In software development of configurable systems, effective software testing is essential. As high configurability entails high testing effort, effective testing is required to meet cost constraints while ensuring satisfactory end product quality. In this paper, we present an initial study on the potential of using statistical testing techniques for improving the efficiency of test selection for configurable software. The study aims to answer whether statistical testing can reduce the effort of localizing the most critical software faults, seen from user perspective. We use probabilistic transition system as the formalism for modeling a probabilistic behavior of the system, and usage models to detect faults that would impact users the most. We present an exemplary case study used to assess the performance of statistical test selection compared to manual practice.

Domain-Independent Method of Detecting Inconsistencies in SBVR-Based Business Rules
Pavan Kumar Chittimalli and Kritika Anand
(Tata Consultancy Services, India)
Traditionally, business rules are expressed informally in English, captured eventually, as a part of UML use-cases. Detecting anomalies in business rules is extremely difficult to automate, due to their informal nature, and manually error-prone due to the size and complexity. In recent times, business rules are being expressed increasingly using standard representations (such as Semantics of Business Vocabularies and Rules (SBVR)). We present a method to detect inconsistencies amongst the rules, based on the model checking. We exploit the First Order Logic (FOL) basis of SBVR representation to propose a method that is independent of the business domain. We present a case-study of business rules for well-known example of car-rental, and our method shows promising results to detect inconsistencies.

ForMABS 2016 – Proceedings

International Workshop on Formal Methods for Analysis of Business Systems (ForMABS 2016)

Frontmatter

Invited Talks

Full Papers