Formal engineering methods are intended to o?er e?ective means for integ- tion of formal methods and practical software development technologies in the context of software engineering. Their purpose is to provide e?ective, rigorous, and systematic techniques for signi?cant improvement of software productivity, quality, and tool supportability. In comparison with formal methods, a distinct feature of formal engineering methods is that they emphasize the importance of the balance between the qualities of simplicity, visualization, and preciseness for practicality. To achieve this goal, formal engineering methods must be - veloped on the basis of both formal methods and existing software technologies in software engineering, and they must serve the improvement of the softwa- engineering process. ICFEM 2008 marks the tenth anniversary of the ?rst ICFEM conference, which was held in Hiroshima in 1997. It aims to bring together researchers and practitioners who are interested in the development and application of formal engineering methods to present their latest work and discuss future research directions. The conference o?ers a great opportunity for researchers in both formal methods and software engineering to exchange their ideas, experience, expectation and to ?nd out whether and how their research results can help advance the state of the art.

This volume contains the proceedings of Formal Methods 2008, the 15th Inter- ? nationalSymposiumonFormalMethods, organizedbyAbo AkademiUniversity, Turku, Finland, during May 26-30, 2008. The series of Formal Methods conf- ences is supported by FME (Formal Methods Europe), an independent asso- ation which aims to stimulate the use of, and the research on, formal methods for system development. The ?rst event in this series was VDM Europe, held in 1987. The scope of the symposium has grown since then, encompassing all aspects of software and hardware that are amenable to formal analysis. As inpreviousyears, this symposiumbroughttogetherinnovatorsandprac- tionersinprecisemathematicalmethodsforsoftwaredevelopment, academicand industrial users as well as researchers, tool developers and vendors. We received 106 submissions from 24 countries, a demonstration of the international nature of the event. Each submission was carefully refereed by at least three reviewers. The Programme Committee ?nally selected 23 papers for presentation at the symposium after what was sometimes really extensive discussion We would like to extend our thanks once more to all the members of the Programme Comm- tee and to all the reviewers for their excellent and e?cient work. (The names of all involved appear over the page.) Apart from the regular papers, there were ?ve invited talks at the symposium, given by Arvind, Shmuel Katz, Paolo Br- ciani, Jay Misra, and Dawson Engler. Arvind and Katz also submitted papers to accompany their talks and these are included in the volume. The Formal Methods 2008 symposium also included various related even

This volume records the 10th Anniversary Colloquium of UNU/IIST, the Int- nationalInstituteforSoftwareTechnologyoftheUnitedNationsUniversity,held in Lisbon, Portugal, March 18-21, 2002. Armando Haeberer, then Chairman of the board of UNU/IIST, conceived the idea of an international meeting in ce- brationoftheinstitute's10thanniversary. HewasworkinginLisbonatthistime andheproposedtoholdthemeetingthere,notleastbecausethePortugueseg- ernment had been one of the major sponsors of the institute, right from the very beginning. The aim of the meeting, organized by the Board of UNU/IIST, was twofold. First, the institute's research work should be re-assessed and diss- inated. Second, the future role of UNU/IIST's research area, formal methods, should be discussed. Role of Formal Methods. Over at least three decades of development, the c- ception of what role formal methods should play in software engineering seems to have changed dramatically, in?uenced by both advocates and detractors. - ginning with a fundamentalist view that contested the genuineness of any 'n- formal' practice, dismissing it as an inappropriate contribution to the as yet ill-de?ned corpus of so-called software engineering, the conception of what this role should be has apparently evolved to a less naive engineering viewpoint. - day, as these theoretical methods acquire a new maturity and breadth of use, many of their advocates appear to be questioning their direct application by software practitioners, often considering it to be nonmandatory, and sometimes even nonadvisable. It appears that, together with the said maturation of the theoretical results and constructions, the perspective of their role within a far more complex picture of the software development activity has also matured.

ETAPS2000wasthe third instanceofthe EuropeanJointConferenceson Theory and Practice of Software. ETAPS is an annual federated conference that was established in 1998 by combining a number of existing and new conferences. This year it comprised v e conferences (FOSSACS, FASE, ESOP, CC, TACAS), ve satellite workshops (CBS, CMCS, CoFI, GRATRA, INT), seven invited lectures, a panel discussion, and ten tutorials. The events that comprise ETAPS address various aspects of the system - velopment process, including speci cation, design, implementation, analysis, and improvement. The languages, methodologies, and tools which support these - tivities are all well within its scope. Die rent blends of theory and practice are represented, with an inclination towards theory with a practical motivation on one hand and soundly-based practice on the other. Many of the issues involved in software design apply to systems in general, including hardware systems, and the emphasis on software is not intended to be exclusive.

This book focuses on the clarification of what actually a handbook is, the systematic identification of what ought to be considered as "settled knowledge" (extracted from historic repositories) for inclusion into such a handbook, and the "assembly" of such identified knowledge into a form which is fit for the purpose and conforms to the formal characteristics of handbooks as a "literary genre". For many newly emerging domains or disciplines, for which no handbook with normative authority has yet been defined, the question arises of how to do this systematically and in a non-arbitrary manner. This book is the first to reflect upon the question of how to construct a desktop handbook. It is demonstrated how concept analysis can be used for identifying settled knowledge as the key ingredient by utilizing the assembled data for classification; a presentation scheme for handbook articles is developed and demonstrated to be suitable. The sketched approach is then illustrated by an example from the railway safety domain. Finally, the limitations of the presented methods are discussed. The key contribution of this book is the (example illustrated) construction method itself, not the handbook, which would result from a highly detailed and thoroughly comprehensive application of the method.