Monday, 26th November 2001
Behavioral Verification with BOBJ and Kumo
Joseph Goguen, Kai Lin, and Grigore Rosu
Practical Machine Learning for Software Engineering
Theory and Practice of Software Architectures
Jose Luiz Fiadeiro, Antonia Lopes and Michel Wermelinger
Reading between the lines: reading and understanding computer programs
2 NASA Ames Research Center - RIACS
Automated Software Engineering Group
Building 269, Room 230
Mail Stop 269-2
Moffett Field, CA 94035-1000, USA
Good implementations often fail to strictly satisfy their specifications, but instead satisfy them only "behaviorally," in the sense of appearing to satisfy them under all members of a certain set of "experiments". Consequently behavioral specifications and behavioral proofs can often be simpler than ordinary specs and proofs. BOBJ is a new member of the OBJ family, which supports behavioral algebraic specification by providing a language, an interpreter, and some algorithms, while the Kumo system extends this to first order behavioral logic, and in addition, generates interactive websites that document the proofs that it produces. This tutorial will describe some basics of "hidden algebra," which is the formal foundation for BOBJ and Kumo, and number of examples, as well as some of the design principles used in building these systems, including parameterized programming and algebraic semiotics.
Machine learning (ML) is not hard and should be a standard part of any software engineer's toolkit. Software engineers can use machine learners to simplify systems development. This tutorial explains how to use ML to assist in the construction of systems that support classification, prediction, diagnosis, planning, monitoring, requirements engineering, validation, and maintenance. Case study material will be presented using examples from software fault estimation, software time estimation, software risk reduction, and electrical diagnosis systems. This tutorial is industrial practioner-oriented. For example, most of its materialis suitable for the AI-novice or the technical manager of software engienering projects. Also, the tutorial explores how to use machine learning in "data-starved" domains; lacks the large datasets needed traditional machine learning. Many software engineering companies operate in such data-starved domains where learning must be proceeded by a modeling process to generate a model we can use to generate data sets. Machine learning for software engineering is practical when both the modeling and learning stages are simple and inexpensive. This tutorial presents such simple and inexpensive techniques.
This tutorial presents mathematical techniques as a toolbox for software architects, and as a foundation for ADL-independent application frameworks to develop architectural design environments. More precisely, a categorical semantics that builds on Goguen's approach to General Systems Theory and other algebraic approaches to specification, concurrency, and parallel program design, is proposed for the formalisation of concepts related to the gross modularisation of complex systems like "interconnection" (in particular connectors in the style defined by Allen and Garlan), "configuration", "instantiation", and "composition". This semantics is, essentially, ADL-independent, setting up criteria against which formalisms and tools can be evaluated according to the support that they provide for architectural design. In particular, it clarifies the role that the separation between computation and coordination plays in supporting architecture-driven approaches to software construction and evolution. It also leads to useful generalisations of the notion of connector, like higher-order connectors and the use of multiple formalisms in the definition of the glue and the roles, which allows connectors to be applied to programs or system components that can be implemented in different languages or correspond to "real-world" components. Finally we show how, based on the proposed categorical semantics, architectural notions can be put at the service of a software development method that ATX Software has been putting together for systems that need to be very agile in reacting to changes in business requirements. The intended audience for our tutorial are all those ASE participants who are interested in SA, and more specifically, on rigorous approaches to architecture-based design and development of software systems. The participants are not assumed to have any prior knowledge of Category Theory but are supposed to feel at ease with mathematical and logical notions at the level of an introductory course in discrete mathematics. We assume that participants are familiar with elementary notions of Software Architecture.
Jose Luiz Fiadeiro is Professor for Computing Science at the University of Lisbon. His research interests include software specification formalisms and methods, especially as applied to component-based, reactive systems, and their integration in the wider area of General Systems Theory. His main contributions have been in the formalisation of specification and program design techniques and of their underlying modularisation principles, namely in connection to Software Architectures. These research interests have been pursued in the context of several national and international projects. He has published more than 70 papers in these areas. He has also co-authored and presented two tutorials on the formalisation of object-oriented modelling techniques at OOPSLA and Object World UK, and tutorials on coordination contracts at OOPSLA'99, OOPSLA'00, TOOLS'01, and ECOOP'01.
Antonia Lopes and Michel Wermelinger were PhD students of J. L. Fiadeiro, working on modular specification of reactive systems and on reconfiguration of software architectures, respectively. They have both published several papers on these subjects and presented their work at international conferences. They both have a considerable experience of teaching in undergraduate programmes. They are now Assistant Professors at the Computer Science Departments of the University of Lisbon and the New University of Lisbon (UNL), respectively. M. Wermelinger is currently a consultant to ATX Software SA under a contract between ATX and UNL.
Most software development is actually maintenance and enhancement of existing programs. And half of maintenance effort goes into understanding the program to be enhanced and the changes being made to it. Consequently, program reading is an essential skill for software developers, but it is rarely if ever directly taught. The objective of this tutorial is to improve the code reading skills for practicing software maintainers and developers. Synchronized Refinement is a systematic, mature, and validated collection of techniques for program understanding. It comprises methods for program analysis, incorporation of domain knowledge, representation, and annotation. It is used in the tutorial as a framework for integrating a collection of program understanding techniques. Particular techniques presented include how to unravel program control flow, how to wade through ripple effects, how to record understanding as it is obtained, how to make use of domain knowledge, and how to extract an architecture from a program. The whole tutorial is presented in the context of example program fragments taken from real software systems.