Powered by
2nd FME Workshop on Formal Methods in Software Engineering (FormaliSE 2014),
June 3, 2014,
Hyderabad, India
2nd FME Workshop on Formal Methods in Software Engineering (FormaliSE 2014)
Frontmatter
Message from the Chairs
The software industry has a long-standing and well-earned reputation for failing to deliver on its promises and it is clear that still nowadays, the success of software projects with the current technologies cannot be assured. For large complex projects ad hoc approaches have proven inadequate to assure the correct behavior of the delivered software. The lack of formalization in key places makes software engineering overly sensitive to the weaknesses that are inevitable in the complex activities behind software creation. Aids to precision in each phase of software development and crosschecking are essential, and this is precisely one the objectives of formal methods.
The main goal of this workshop is to foster integration between the formal methods and the software engineering communities with the purpose to examine the link between the two more carefully than is currently the case.
Invited Talk
Software Reliability via Machine Learning (Invited Talk)
Aditya V. Nori
(Microsoft Research, India)
Computing good invariants is key to effective and efficient program verification. In this talk I will describe our experiences in using machine learning techniques (support vector machines, linear regression) for computing invariants useful for program verification as well as for fine tuning verification tools.
@InProceedings{FormaliSE14p1,
author = {Aditya V. Nori},
title = {Software Reliability via Machine Learning (Invited Talk)},
booktitle = {Proc.\ FormaliSE},
publisher = {ACM},
pages = {1--2},
doi = {},
year = {2014},
}
Integration of Formal Methods in Software Engineering I
Formal Specification Comprehension: The Art of Reading and Writing Z
Andreas Bollin and Dominik Rauner-Reithmayer
(University of Klagenfurt, Austria; Carinthia University of Applied Sciences, Austria)
Formal Methods have been developed to provide systematic and rigorous techniques for software development. They found their place in document-driven development processes as well as in the agile world. However, reading, understanding and working with a formal specification still turns out to be a real challenge.
This paper tries to identify the underlying cause and argues that comprehensibility of a specification is one of the key factors. It presents some first findings of an extensive study investigating the readability of Z specifications and comes up with a set of recommendations in writing formal specifications so that the syntactic gap between the mathematics and the natural language requirements description can be bridged more easily.
@InProceedings{FormaliSE14p3,
author = {Andreas Bollin and Dominik Rauner-Reithmayer},
title = {Formal Specification Comprehension: The Art of Reading and Writing Z},
booktitle = {Proc.\ FormaliSE},
publisher = {ACM},
pages = {3--9},
doi = {},
year = {2014},
}
Integration of Formal Methods in Software Engineering II
Flexible Modular Formalization of UML Sequence Diagrams
Luciano Baresi, Mohammad Mehdi Pourhashem Kallehbasti, and Matteo Rossi
(Politecnico di Milano, Italy)
UML Sequence Diagrams are one of the most commonly used type of UML diagrams in practice. Their semantics is often considered to be straightforward, but a more detailed analysis reveals diverse interpretations. These different choices must be properly supported by verification tools. This paper describes a formal framework for capturing semantic choices in a precise and modular way. The user is then able to select the semantics of interest, mix different interpretations, and analyze diagrams according to the chosen solution. This solution is supported by Corretto, our UML verification environment, to allow the user to play with different semantics and prove properties on Sequence Diagrams, accordingly.
@InProceedings{FormaliSE14p10,
author = {Luciano Baresi and Mohammad Mehdi Pourhashem Kallehbasti and Matteo Rossi},
title = {Flexible Modular Formalization of UML Sequence Diagrams},
booktitle = {Proc.\ FormaliSE},
publisher = {ACM},
pages = {10--16},
doi = {},
year = {2014},
}
From an Abstract Specification in Event-B toward an UML/OCL Model
Imen Sayar and Mohamed Tahar Bhiri
(University of Sfax, Tunisia; University of Lorraine, France)
The formal approach of software development promotes getting proved correct software. It faces the shortcomings of the classical approach concerning the ambiguity of the requirements document, the risk of errors distributed to all phases and the high testing cost (because of late detection of such errors). However, this approach poses problems mainly related to the participation of various actors not necessarily professionals in formal methods, maintenance and especially the development of an "optimal" refinement strategy. To overcome the limitations of these two approaches, we propose a hybrid approach that combines the formal approach (Event-B) and the classical approach (UML/OCL). Upstream phases of our approach include: Rewriting the requirements document, Refinement strategy, Abstract specification, Horizontal refinement and Validation. Downstream phases contain the Construction of a UML/EM-OCL model, Refinement, Integration of design and implementation decisions, Coding and Integration. In this paper, we show the feasibility of our approach on a case study: An Electronic Hotel Key System (SCEH). The problem of transition from formal (Event-B) to the semi-formal (UML/OCL) is processed by our OCL extension called EM-OCL.
@InProceedings{FormaliSE14p17,
author = {Imen Sayar and Mohamed Tahar Bhiri},
title = {From an Abstract Specification in Event-B toward an UML/OCL Model},
booktitle = {Proc.\ FormaliSE},
publisher = {ACM},
pages = {17--23},
doi = {},
year = {2014},
}
Generating Supportive Hypotheses in Introducing Formal Methods using a Software Processes Improvement Model
Shigeru Kusakabe, Hsin-Hung Lin, Yoichi Omori, and Keijiro Araki
(Kyushu University, Japan)
We are investigating the effective facilitation methodology for the introduction of formal methods into actual software developments.
One of the important issues is how to define and develop an adequate development process with formal methods.
In this paper, we discuss this issue from a view point of software process improvement using a standard development process model, CMMI-DEV, which is a compilation of best practices in software development.
We expect using the standard process model as a reference can facilitate common understanding for the advantages of formal methods and the comparison between actual instances of software process with formal methods.
This approach leads to the exploitation of knowledge and findings obtained in the successful cases.
We generate supportive hypotheses in the effect of formal methods on software development processes by using the standard improvement model.
Then, we weakly examine them with a combination of a small-scale process, which has a strong relation to the organization level process, and a model-oriented formal method, VDM.
@InProceedings{FormaliSE14p24,
author = {Shigeru Kusakabe and Hsin-Hung Lin and Yoichi Omori and Keijiro Araki},
title = {Generating Supportive Hypotheses in Introducing Formal Methods using a Software Processes Improvement Model},
booktitle = {Proc.\ FormaliSE},
publisher = {ACM},
pages = {24--30},
doi = {},
year = {2014},
}
Analysis and Verification
Using mCRL2 for the Analysis of Software Product Lines
Maurice H. ter Beek and Erik P. de Vink
(ISTI-CNR, Italy; Eindhoven University of Technology, Netherlands; CWI, Netherlands)
We show how the formal specification language mCRL2 and its
state-of-the-art toolset can be used successfully to model and analyze
variability in software product lines. The mCRL2 toolset supports
parametrized modeling, model reduction and quality assurance
techniques like model checking. We present a proof-of-concept, which
moreover illustrates the use of data in mCRL2 and also how to exploit
its data language to manage feature attributes of software product
lines and quantitative constraints between attributes and features.
@InProceedings{FormaliSE14p31,
author = {Maurice H. ter Beek and Erik P. de Vink},
title = {Using mCRL2 for the Analysis of Software Product Lines},
booktitle = {Proc.\ FormaliSE},
publisher = {ACM},
pages = {31--37},
doi = {},
year = {2014},
}
Compiling Polychronous Programs into Conditional Partial Orders for ASIP Synthesis
Mahesh Nanjundappa and Sandeep K. Shukla
(Virginia Tech, USA)
Synthesis of application specific hardware which minimizes area while not sacrificing latency or clock speed is a much researched problem. In most of the past works, the hardware is described structurally in hardware description languages with behaviors attached to structures. Since the structure is manually decided, the architect has to decide whether certain components can be reused without increasing latency. For example, if one can prove that certain behaviors never happen at the same time, these behaviors can be mapped to common components, with a simple control state machine determining which behavioral mode the behavior belongs to. Since application specific hardware are used as co-processors for performance boost, and such computations are best described as a data-flow computation (such as signal processing, encryption etc.,), we choose a high level data-flow oriented formal specification language, and use a new semantic model for this specification language, namely conditional partial order graphs. The advantage of our approach is that our specification language MRICDF is graphical, polychronous, has formal semantics, and hence synthesizing its control structure into conditional partial order is a natural fit. Additionally, the specific calculus of constraints in polychronous languages -- namely clock calculus, and associated analysis with Boolean theory of prime implicates, and constraint satisfiability checking with SMT solvers provide us with a natural way of discovering behaviors that belong to disjoint modes, and thereby allow us to reuse components with simple micro-instruction set synthesis. In this paper, we show how MRICDF can be used to formally synthesize such application specific instruction processors. Past approaches to synthesize hardware from the polychronous language SIGNAL were focused on synthesizing logic with hierarchical conditional dependency graphs as internal representation. Unlike those, we are synthesizing an application specific instruction set processor by automated synthesis of control and scheduling data-path.
@InProceedings{FormaliSE14p38,
author = {Mahesh Nanjundappa and Sandeep K. Shukla},
title = {Compiling Polychronous Programs into Conditional Partial Orders for ASIP Synthesis},
booktitle = {Proc.\ FormaliSE},
publisher = {ACM},
pages = {38--44},
doi = {},
year = {2014},
}
Verification and Testing
Formalization of Software Models for Cyber-Physical Systems
Sandeep Neema, Gabor Simko, Tihamer Levendovszky, Joseph Porter, Akshay Agrawal, and Janos Sztipanovits
(Vanderbilt University, USA)
The involvement of formal methods is indispensable for modern
software engineering. This especially holds for Cyber-Physical
Systems (CPS). In order to deal with the complexity and
heterogeneity of the design, model-based engineering is widely
used. The complexity of detailed verification in the final source
code makes it imperative to introduce formal methods earlier in
the design process. Because of the widespread use of customized
modeling languages (domain-specific modeling languages,
DSMLs), it is crucial to formally specify the DSML, and verify if
the model meets fundamental correctness criteria. This is
achieved by specifying behavioral and structural semantics of the
modeling language. Significant model-driven tools have emerged
incorporating advanced model checking methods that can provide
some assurance regarding the quality and correctness of the
models. However, the code generated from these models, using
auto code generators remains circumspect, since the correctness
of the code generators cannot be assumed as a given, and remains
intractable to prove. Therefore, we propose a pragmatic
approach, instead of verifying explicit implementation of code
generator, verifies the correctness of the generated code with
respect to a specific set of user-defined properties to establish that
the code-generators are property-preserving. In order to make the
verification workflow conducive to domain engineers, who are not
often trained in formal methods, we include a mechanism for
high-level specification of temporal properties using pattern-based
verification templates. The presented toolchain leverages
state-of-the-art verification tools, and a small case-study
illustrates the approach.
@InProceedings{FormaliSE14p45,
author = {Sandeep Neema and Gabor Simko and Tihamer Levendovszky and Joseph Porter and Akshay Agrawal and Janos Sztipanovits},
title = {Formalization of Software Models for Cyber-Physical Systems},
booktitle = {Proc.\ FormaliSE},
publisher = {ACM},
pages = {45--51},
doi = {},
year = {2014},
}
Analysis and Testing of PLEXIL Plans
Jason Biatek, Michael W. Whalen, Mats P. E. Heimdahl, Sanjai Rayadurgam, and Michael R. Lowry
(University of Minnesota, USA; NASA Ames Research Center, USA)
Autonomy is increasingly important in missions to remote locations
(e.g., space applications and deep sea exploration) since limited bandwidth and
communication delays make detailed instructions from a remote base (e.g., Earth
or a land base) impractical. The planning systems used for autonomous operation
are difficult to verify and validate because they must create plans for use in a
specific environment and the correct behavior might not be easy to define.
To explore verification and validation of planning systems, we have developed a
verification framework for the PLEXIL plan execution language. The framework
allows us to perform verification and test case generation using Java Symbolic
PathFinder. Using this framework, we have performed
verification, bounded verification and test-case generation for NASA-relevant
PLEXIL plans and discovered two bugs in the PLEXIL language semantics: one in
the definition of the If/Then/Else construct in the Extended PLEXIL language
that could lead to plan deadlocks, and one in the semantics of the core language
that could cause the PLEXIL executive to crash.
@InProceedings{FormaliSE14p52,
author = {Jason Biatek and Michael W. Whalen and Mats P. E. Heimdahl and Sanjai Rayadurgam and Michael R. Lowry},
title = {Analysis and Testing of PLEXIL Plans},
booktitle = {Proc.\ FormaliSE},
publisher = {ACM},
pages = {52--58},
doi = {},
year = {2014},
}
proc time: 0.67