|
|
Sixth International
Conference on |
|
|
Sponsors:
|
Workshop & Tutorials
SVV WorkshopInternational Workshop on Software Verification and Validation (SVV)DescriptionThe workshop will focus on theoretical techniques, practical methods as well as case studies for verification of conventional and embedded software systems. The goal of this workshop is to promote discussion on novel combinations of different methodologies for verifying and validating software systems, as well as study the individual contribution of each of thes methodologies.LocationTBDDate and TimeMonday, Nov-08-04, 8:30am - 5:00pm (one-day)OrganizerSupratic Mukhopadhyay (NASA IV&V Center and West Virginia University, USA)Abhik Roychoudhury (National University of Singapore, Singapore) Tutorial 1Model-based Development: Combining Engineering Approaches and Formal TechniquesDescriptionModel-based development adds the structuring and preciseness of formal approaches to the development process while being driven by the models of the application domain instead of mathematical formalisms. In this tutorial we show how a model-based approach can help to systematically define system boundaries, specify an abstract behavior of the system and the enviornment, ensure the suitability of the model, and repeatedly enhance the system with design decisions. The main objective of this tutorial is to demonstrate the methodical support gained from the application of tool-supported formal techniques to engineering methods in the development of reactive systems. We focus on how the complexity of the design process can be reduced by breaking it up into different steps, each concentrating on a special aspect of the development. A special emphasis is put on how CASE support can simplify those steps. As illustrating example we use the BART(Bay Area Rapid Transfer) case study, describing the requirements of a system controlling the speed and acceleration selection for fully-automated trains; the CASE-tool AutoFocus - selected as best formal tool at FM'99 and used in several industrial projects - is used to demonstrate the state of the art in tool support.LocationTBDDate and TimeMonday, Nov-08-04, 8:30am - 12:00pm (half-day)PresenterBernhard Schatz, Fakultat fur Informatik, TU Munchen, Germany Bernhard Schaetz is a Senior Researcher at the Computer Science Insitute of the Technische University Munchen. He furthermore works as a consultant for industrial partners and is a co-founder of a university spin-off for embedded software. His current research focuses on the application of formal techniques in the engineering process. His work aims at the construction of CASE tools for a model-based software engineering process for embedded systems. Results of his research are incorporated in the development of the AutoFOCUS tool.Tutorial 2Tutorial on the RAISE Language, Method, and ToolsDescriptionRAISE - Rigorous Approach to Industrial Software Engineering - was first developed in European collaborative projects during 1985-94. Since then a new set of free, open-source, portable tools has been developed, and a range of developments have been carried out. This tutorial introduces the language and method, and demonstrates the range of software life-cycle activities supported by the tools. These include generation of specifications from UML class diagrams, validation and verification of specifications, refinement, prototyping, execution of test cases, mutation testing, generation of documents, and generation of program code in C++ by translation. A comprehensive user guide is also available.LocationTBDDate and TimeMonday, Nov-08-04, 1:30pm - 5:00pm (half-day)PresenterChris George, UNU/IIST Chris George worked as a software engineer and project manager for telecommunications and software companies in England and Denmark during 1979 to 1994. In 1994 he joined the International Institute for Software Technology of the United Nations University (UNU-IIST) in Macao, China, as a Senior Research Fellow. He has been the Director a.i. of UNU-IIST since February 2003. He was one of the main original developers of RAISE and has been using and teaching it at UNU-IIST, as well as developing the new RAISE tools. He was the main author of the book "The RAISE Development Method" and main editor of the book "Specification Case Studies in RAISE". He has given many courses and tutorials on it and on other subjects, including project management. He was PC co-chair of ICFEM02, and has served on the PCs of various FM conferences, such as FME and IFM.Tutorial 3Model-based Testing with Spec#DescriptionThis tutorial will introduce model-based testing, using the Spec# modeling language and the Spece Explorer test tool. Spec# is an extension of C# with additional constructs (preconditions, postconditions, and invariants) and for executable model programs (very high level data types including sets, sequences, and maps, and also nondeterministic choice). Spec Explorer can be used to investigate the properties of Spec# models using techniques similar to model checking, to generate test suites from Spec# models, and to perform conformance tests by executing the Spec# model together with the implementation under test, using the model porgram as the oracle. Spec Explorer can be configured to implement different testing strategies and achieve different coverage criteria.LocationTBDDate and TimeTuesday, Nov-09-04, 8:30am - 12:00pm (half-day)PresenterJonathan Jacky, University of Washington Jonathan Jacky is a research scientist at the University of Washington in Seattle, experienced in the develeopment of safety-critical medical systems. He is the author of The Way of Z, a textbook on formal methods. In 2003-2004 he is a Visiting Researcher in the Foundations of Software Engineering group at Microsoft.Tutorial 4Formal Engineering for Industrial Software Development -- An Introduction to the SOFL Specification Language and MethodDescriptionFormal methods have been developed as a rigorous approach to computer systems development over last three decades, but have been facing strong challenges in fighting for industrial acceptance at large. Most commonly used formal methods do not offer effective and comprehensible structuring mechanism for building complex systems; formal refinement rules are insufficient in dealing with real development situations; and formal verification is not capable of validating systems, although it may be useful in verifying the correctness of programs against their formal specifications. To support application of formal methods in industrial setting, many open problems remain to be resolved. Over last 10 years, we have developed the SOFL specification language and method for software development, aiming to address those problems. As a specification language, SOFL, standing for Structured Object-Oriented Formal Language, integrates VDM-SL, Data Flow Diagrams, and Petri Nets to provide an intuitive, rigorous, and comprehensible formal notation for specifications at different levels. As a method, it combines structured methods and object-oriented methods, and advocates an evolutionary approach to constructing specifications; it also integrates the idea of formal proof and commonly used verification and validation techniques, such as testing and reviews, to offer rigorous but practical verification techniques. This tutorial will provide a systematic introduction to the SOFL specification language and the associated method for industrial software development, explain how conventional formal methods can be incorporated into the entire software process to achieve rigor, comprehensibility, and tool supportability of the commonly used modeling and verification techniques, and discuss future research and development directions in the area of Formal Engineering Methods.LocationTBDDate and TimeNov-09-04, 1:30pm - 5:00pm (half-day)PresenterShaoying Liu, Hosei University Shaoying Liu has designed and developed the SOFL specification language and method, which is so far the only method to have successfully addressed most of the engineering issues in software development using formal methods in a systematic manner. He has served as general chairs and program co-chairs, respectively, for several international conferences, including ICFEM'97, ICFEM'98, ICFEM'00, ICECCS'99, ICECCS'00, ICECCS'02, and PC member for numerious conferences, including FM'99, FME'03, IFM series, APSEC'01, 02, and 03. He has published over 70 papers on Software Engineering and Formal Methods, and written and edited four books on Formal Engineering Methods. He is a member of IEEE Computer Society and Software Science Society of Japan. |
|
Send mail to schulte@microsoft.com
with questions or comments about this web site.
|
