P179 - FM+AM`2010 - Second International Workshop on Formal Methods and Agile Methods
Autor*innen mit den meisten Dokumenten
Auflistung nach:
Neueste Veröffentlichungen
- KonferenzbeitragAgile formality: A "Mole" of software engineering practices(FM+AM`2010 – Second International Workshop on Formal Methods and Agile Methods, 2010) Bianco, Vieri del; Stosic, Dragan; Kiniry, Joseph R.Members of the agile programming and formal methods communities do not always see eye-to-eye. These two communities often do not talk to or learn from each other. Only recently, as highlighted by the September 2009 issue of IEEE Software, the IFIP workshop on balancing agility and formalism in software engineering, and the first edition of the international workshop for formal methods and agile methods, ideas from the two communities begun synthesize. While the problem-solving approaches and psychological attitudes of members of the two communities differ widely, we exploit this clash of viewpoints, creating a new development processes that actually blends, rather than mashes together, best practices from the two worlds. This paper summarizes our process and a supporting complex case study, showing that it is not only possible, but tasty, to combine the “chili pepper” of formal methods and the “chocolate” of agile programming, thus producing a tasty “Mole” (as in the highlyspiced Mexican sauce) of software engineering practices.
- KonferenzbeitragAre formal methods ready for agility? A reality check(FM+AM`2010 – Second International Workshop on Formal Methods and Agile Methods, 2010) Gorm Larsen, Peter; Fitzgerald, John; Wolff, SuneThe integration of agile software development techniques with formal methods has attracted attention as a research topic. But what exactly is to be gained from attempting to combine two approaches which are seen as orthogonal or even opposing, and to what extent do formal methods already support the principles of agility? Based on the authors' experience in applying lightweight tool-supported formal methods in industrial projects, this paper assesses the readiness of formal methods technologies for supporting agile techniques and identified areas in which new research could improve the prospects of synergy between the two approaches in future.
- KonferenzbeitragAn experience on formal analysis of a high-level graphical SOA design(FM+AM`2010 – Second International Workshop on Formal Methods and Agile Methods, 2010) Beek, Maurice H. ter; Mazzanti, Franco; Sulova, AldiIn this paper, we present the experience gained with the participation in a case study in which a novel high-level design language (UML4SOA) was used to produce a service-oriented system design, to be model checked with respect to the intended requirements and automatically translated into executable BPEL code. This experience, beyond revealing several uncertainties in the language definition, and several flaws in the designed model, has been useful to better understand the hidden risks of apparently intuitive graphical designs, when these are not backed up by a precise and rigorous semantics. The adoption of a rigorous or formal semantics for these notations, and the adoption of formal verification methods allow the full exploration of designs which otherwise risk to become simple to draw and update, but difficult to really understand in all their hidden ramifications. Automatic formal model generation from high level graphical designs is not only desirable but also pragmatically feasible e.g. using appropriate model transformation techniques. This is particularly valuable in the context of agile development approaches which are based on rapid and continuous updates of the system designs.
- Editiertes Buch
- KonferenzbeitragImproved underspecification for model-based testing in agile development(FM+AM`2010 – Second International Workshop on Formal Methods and Agile Methods, 2010) Faragó, DavidSince model-based testing (MBT) and agile development are two major approaches to increase the quality of software, this paper considers their combination. After motivating that strongly integrating both is the most fruitful, the demands on MBT for this integration are investigated: The model must be underspecifyable and iteratively refineable and test generation must efficiently handle this. The theoretical basis and an example for such models is given. Thereafter, a new method for MBT is introduced, which can handle this more efficiently, i.e., can better cope with nondeterminism and also has better guidance in the model traversal. Hence it can be used in agile development, select more revealing tests and achieve higher coverage and reproducibility.
- KonferenzbeitragState-based coverage analysis and UML-driven equivalence checking for C++ state machines(FM+AM`2010 – Second International Workshop on Formal Methods and Agile Methods, 2010) Heckeler, Patrick; Behrend, Jörg; Kropf, Thomas; Ruf, Jürgen; Rosenstiel, Wolfgang; Weiss, RolandThis paper presents a methodology using an instrumentation-based behavioral checker to detect behavioral deviations of a C++ object implementing a finite state machine (FSM) and the corresponding specification defined as a UML state chart. The approach is able to link the source code with the appropriate states and provides a coverage analysis to show which states have been covered by unit, system and integration tests. Furthermore, the approach provides statistical information about the distribution of covered lines of code among all included files and directories. As a proof of concept the presented approach has been implemented in terms of a C++-library and has been successfully applied to OPC UA, an industrial automation infrastructure software.