| | | Abstracts of Talks |
José Luiz FiadeiroService-Oriented Computing is the paradigm that is intended to replace object-oriented and component-based development for distributed computing and e-business processing in agile, rapidly customisable networks of Web resources. (e-)Services are considered to be autonomous, platform-independent, computational entities that can be described, published, discovered, and dynamically assembled for the purpose of developing massively distributed, interoperable, evolvable systems.
Software Specification and Design Group
Department of Computer Science
University of Leicester
Starting with the identification of some of the shortcomings of object-oriented methodology and component-based technology to address the challenges of supporting the engineering and deployment of e-Services, we suggest that alternative approaches can be found in what we call "coordination methodologies and technologies" - a set of modelling primitives, design principles, design patterns, and analysis techniques that we have been developing for supporting the construction and evolution of complex software systems that need to operate in very volatile and dynamic environments.
Dominique Duval (LMC, IMAG, Grenoble), Hélène Kirchner (LORIA, Nancy), and Christian Lair (Université de Paris 7).This talk contains some hints for a simple and coherent definition of overloading, coercions and subsorts, in an equational specification context.
It does not contain any attempt at unifying existing approaches [Mosses, 1992].
It is motivated by the decorated equational logic in [Hintermeier, Kirchner, Kirchner, 1998].
And it relies (implicitly) on diagrammatic specifications (l'Alpe d'Huez) [Duval, Lair, 2002], and zooms (Frauenchiemsee) [Duval, Lair, Oriat, Reynaud, 2003].
http://www-lmc.imag.fr/lmc-cf/Dominique.Duval/publis.html is a pointer to the papers:
In some weeks, the paper
will be available at the same address.
Thorsten AltenkirchWe introduce the notion of a container, in the category of Sets a container is a parametric datatype T of the form T(X) = Sigmax in S.P(s) -> X, where S is the set of shapes and P(s) is the family of positions - this can be easily generalized to multi-variate containers. All containers are functors, the constant and identity functor are containers and containers are closed under ×,+, initial algebra, terminal coalgebras and exponentiation with a constant -- hence all strictly positive datatypes are containers. We define container morphisms and show that the extension functor into the category of endofunctors is full and faithful. This gives a useful representation result for polymorphic functions between containers.
University of Nottingham, England
Containers provide a canonical representation for datatypes. One interesting application is generic programming. As an example we develop the theory of datatypes with holes which is useful for generalizing editing operations on trees like Huet's zipper. As already McBride noticed a datatype with a hole is its formal derivative. We use containers to define an abstract definition of a tangent and derive the laws of derivative from this. Closing containers under quotients of positions leads to the notion of abstract containers. Interestingly, the container which plays the role of ex in calculus turns out to be the type of multisets or bags.
Containers and the associated constructions work in any locally cartesian category which is locally finitely presentable (LFP). In current work we investigate whether LFP-ness can be replaced by the W-types, which would include more categories, in particular realizability categories.
My presentation is based on joint work with Michael Abbot, Neil Ghani and Conor McBride which has been published in the proceedings of FOSSACS 03 and TLCA 03.
My slides are available at: http://www.cs.nott.ac.uk/~txa/talks/menorca.ps
The relevant papers can be found on my publication page, http://www.cs.nott.ac.uk/~txa/publ/
Dominique MéryAbstractions techniques allow one to get a simpler view of a system but we cn also used refinement techniques for contructing in an incremental way, complex software systems. We define a class of predicate diagrams that represent abstractions of--possibly infinite-state--reactive systems. Our diagrams support the verification of safety as well as liveness properties. Non-temporal proof obligations establish the correspondence between the original specification, whereas model checking can be used to verify behavioral properties. We define a notion of refinement between diagrams that is intended to justify the top-down development of systems within the framework of diagrams. The method is illustrated by a number of mutual-exclusion algorithms, but tools are still missing. Further works will improve those techniques especially by developing tools.
LORIA, Université Henri Poincaré Nancy 1
email: mery@loria.fr
Links: http://www.loria.fr/~mery
Carlos CaleiroWe start by overviewing the main ideas and results about the fibring mechanism for combining logics, including soundness and completeness preservation theorems. However, although quite powerful, fibring suffers from an anomaly usually known as "the collapsing problem". Indeed, ever since the first accounts of fibring, it could be noticed that fibring a 2-valued with a 3-valued logic would yield no fibred 3-valued models, or that the fibring of classical with intuitionistic logic would collapse into just classical logic. In [Sernadas,Rasga and Carnielli] modulated fibring has been introduced and shown to avoid these collapses, by means of a very careful use of adjunctions between lattice structured models. In this work, we propose a structurally simpler alternative to solve the semantic collapse problem by adopting a more general notion of fibred semantics using cryptomorphisms, in a spirit similar to the mechanisms for combining parchments in the theory of institutions. In particular, we show that the novel notion of cryptofibring encompasses the original definition of fibred model, while admiting also (initial) amalgamated models that can be used to show that the above mentioned collapses are no longer present. This talk reports on ongoing joint work with Jaime Ramos, Amilcar Sernadas and Cristina Sernadas.
Center for Logic and Computation, Department of Mathematics
IST - Technical University of Lisbon, Portugal
SLIDES http://ccal.math.ist.utl.pt/slides/cryptofibring.pdf
Reiko HeckelOpen distributed systems are often built according to the service-oriented architectural style (SoA) underlying Web services or Jini. This talk proposes to model the software architecture service-oriented applications based on UML notation, with graph transformation as the underlying semantic model. Based on this semantics we discuss support for model-driven development, i.e., the refinement of scenarios at the level of the business architecture into SoA-specific scenarios ones through reachability analysis.
University of Paderborn, Germany
http://www.upb.de/cs/reiko.html
Slides available at: http://www.upb.de/cs/ag-engels/ag_engl/People/Heckel/talks/ifip1.3_Menorca03.pdf
Martin Grosse-RhodeThe mission of a research project is determined to a large extent by its conditions and circumstances. Thereby a fundamental distinction can be made between academic and industrial research, where the latter essentially means being funded 100buyer) of the research project. The motivations, problem definitions, scopes, time periods, and success criteria in applied research, understood as industrial research, are rather different from the ones found in academic research. The often posed question how to bridge the gap between theory and practice could accordingly be reduced to the question how to bridge the gap between academic and industrial research.
Fraunhofer Institut fuer Software- und Systemtechnik - ISST
Berlin, Germany
email: Martin.Grosse-Rhode@isst.fhg.de
URL: http://www.isst.fhg.de/~mgrosse
Having moved from academia to an applied research institute that is mainly devoted to industrial research, I give in the talk a quite personal experience report on the differences of these types of research projects. As a case study I present a model-oriented method for the development of component-based systems that has been designed by the institute for a company in the automotive industry. As one of the conclusions I try to derive theoretical questions that arose from this and related projects, and whose clarification - for instance by academic researchers - could result in a substantial improvement for the further development of such applied methods.
slides: Meeting-2003-Menorca-Grosse-Rhode.pdf
Manuel Clavel, Narciso Marti-Oliet, and Miguel PalominoThis work is both a development and an application of ideas introduced in "Reflective Metalogical Frameworks", by D. Basin, M. Clavel, and J. Meseguer [to appear in "ACM Transactions on Computational Logic"]. First, we provide several extensions to the metalogical reasoning principles proposed in that paper. In particular, while the original paper only considered metatheorems about equational theories which are related by inclusion, our reflective methodology can also deal with metatheorems about theories which are unrelated by inclusion. We also provide an extension of their parameterization mechanisms.
Departamento de Sistemas Informaticos y Programacion
Universidad Complutense de Madrid, Spain
Then, we apply this reflective methodology in two case studies. As is well-known, equational specifications can be related in different ways, and these relations can be informally formulated as metatheorems of equational logic. We show that some of these semantic relations can be formalized as theorems of the universal theory of membership equational logic (a theory that can simulate the deductions of all theories in the logic, including itself), and that they can be logically proved in a way that mirrors their corresponding proofs at the metalogical level. We also show reflected proofs of different parameterized versions of the deduction theorem for minimal logic of implication.
Dusko PavlovicIn software engineering, complexity is usually dealt with by a separating the design of systems architectures from the development of generic, reusable components and connectors. Some important concerns, however, cut across this two dimensional space, spanned by architectures and components, and do not yield to such separation, but require unified treatment. Security concerns provide many relevant examples of this kind.
Kestrel Institute, Palo Alto
We describe a case study of the Binding Update phase of a proposed protocol for Mobile IPv6. After a brief description of the Mobile IP problem, and the IPv4 solution, that allows for traffic hijacking, we describe the proposed Binding Update protocol in cord calculus. The framework of evolving specifications, briefly described, allows us to analyze behavior of this protocol, as an architectural connector, with respect to the possible attackers. The possibility of traffic hijacking is eliminated by applying a generic protocol transformation, enabled by this framework.
Relevant papers:
Composition and refinement of behavioral specifications. ASE 01 with D. Smith
A compositional logic for protocol correctness. CSFW 01 with N. Durgin and J. Mitchell
On Specification Carrying Software, its Refinement and Composition. IDPT 2002 with M. Anlauff
Guarded transitions in evolving specifications. AMAST 02 with D. Smith
A derivation system for security protocols and its logical formalization. CSFW 03 with A. Datta, A. Derek, J. Mitchell
http://www.kestrel.edu/users/pavlovic/
Michel Bidoit and Rolf HennickerThis talk is a follow-up of the previous talk at the Chiemsee meeting on the Constructor-based Observational Logic COL. Here we develop proof techniques for structured COL-specifications. For this purpose we introduce an institution encoding from the COL institution to the usual institution of many-sorted first-order logic with equality and sort-generation constraints. Using this institution encoding, we can then reduce proofs of consequences of structured specifications built over COL to proofs of consequences of structured specifications written in a simple subset of the algebraic specification language CASL. This means in particular that any inductive theorem prover, such as e.g. Larch or PVS, can be used to prove theorems over structured COL-specifications. Paper:
Michel Bidoit and Rolf Hennicker. Constructor-based Observational Logic. Submitted for publication, June 2003. URL: http://www.lsv.ens-cachan.fr/~bidoit/COL.pdf
D. Pavlovic, Kestrel Institute (dusko@kestrel.edu),This case study applies techniques of formal program development in the style of Kestrel's SpecWare approach, in particular specification refinement and composition, to the problem of concurrent garbage collection. The specification formalism is mainly based on algebraic specification and functional programming paradigms, the imperative aspect is dealt with by using monads. The well-known rely-guarantee mechanism for concurrent processes is realized by way of mutually recursive algebraic specifications.
P. Pepper, Fakultät für Elektrotechnik und Informatik, Technische Universität Berlin (pepper@cs.tu-berlin.de),
D. SmithKestrel Institute (smith@kestrel.edu)
Alexander KurzAlgebras are usually given wrt a signature and logics to specify algebras are easily derived from the signature. Coalgebras are usually given wrt a functor and it is not so clear how to best associate--possibly in a uniform way--a modal logic to a given functor. This problem has been addressed in work by, eg, Moss, Gumm, Roessiger, Jacobs, Pattinson, Cirstea.
University of Leicester, England
The new solution we propose makes use of Stone duality: Roughly speaking, given a functor T on a category C, the modal logic (operators and axioms) is given by the dual of T on the Stone dual of C. This is joint work with Marcello Bonsangue from the University of Leiden.
The consideration of coalgebras over topological spaces is motivated by showing that the so-called descriptive general frames of modal logic are coalgebras over Stone spaces for the Vietoris functor (Plotkin powerspace). This is joint work with Clemens Kupke and Yde Venema from Amsterdam.
Slides available at:
http://www.mcs.le.ac.uk/~akurz/Papers/IFIP-June-03/ifip.dvi,
http://www.mcs.le.ac.uk/~akurz/Papers/IFIP-June-03/ifip.4.ps (4 pages on 1),
http://www.mcs.le.ac.uk/~akurz/Papers/IFIP-June-03/ifip.pdf
The work on Stone coalgebras will appear in the proceedings of CMCS'03 in volume 82 of ENTCS.
A. Edalat, Imperial College, London, UKWe derive a simple domain-theoretic version of the Picard operator and of Picard's theorem for solving the classical initial value problem, which only uses the function space of Scott continuous interval-valued maps of a real variable. The main consequence of the new theorem is that it gives rise, in the Lipschitz case, to fast convergence of approximations by linear step functions to the unique solution when the vector field is approximated by step functions. We show that by flattening the linear step functions into a simple step functions, after each iterate of the Picard operator, and by a suitable approximation of the vector field, one can overcome the blow-up of the number of single-step functions in the approximations to the solution. We report the performance of a simple implementation of the underlying framework, tested on a few examples.
D. Pattinson, LMU Muenchen, Germany
The slides (and probably a pointer to the paper at a later stage) will be made available at
http://siskin.pst.informatik.uni-muenchen.de/~pattinso/Talks/
Bart Jacobs, Joseph Kiniry, Martijn WarnierThis paper aims to raise the level of verification challenges by presenting a collection of sequential Java programs with correctness annotations formulated in JML. The emphasis lies more on the underlying semantical issues than on verification.
Paper URL: http://www.cs.kun.nl/research/reports/info/NIII-R0310.html
Slides URL: http://www.cs.kun.nl/~bart/TALKS/ifip_wg13_03.pdf
Fernando Orejas (work in cooperation with Hartmut Ehrig, Benjamin Braatz, Markus Klein and Martti Piirainen)In this talk I will first introduce a generic component framework that can be used to describe software components for a large class of formal (but also semiformal) specification formalisms. In particular the framework can be instantiated to a given formalism by defining appropriate notions of inclusion and transformatio (or refinement) that satisfy some given properties.
In the second part of the talk I will show the instantiation of this approach to specification frameworks whose semantics can be defined in terms of Algebra Transformation Systems and where the associated refinements can be defined in terms of High-Level Replacement Systems.
Finally, I will present a new semantics for the basic component framework which is inspired on the use of "data constraints" to define the meaning of parameterized specifications. This new semantics allows us to present the meaning of a number of composition operations, including circular composition, in a relative simple and systematic way.
Christine Choppy (U. Paris13, France) and Gianna Reggio (U. Genova, Italy)One of the goals of software engineering is to provide what is necessary to write relevant, legible, useful descriptions of the systems to be developed, which will be the basis of successful developments. This goal was addressed both from informal approaches (providing in particular visual languages) and formal ones (providing a formal sound semantic basis).
Informal approaches are often driven by a software development method, and while formal approaches sometimes provide a user method, it is usually aimed at helping to use the proposed formalism/language when writing a specification. Our goal here is to provide a companion method that helps the user to understand the system to be developed, and to write the corresponding formal specifications.
We also aim at supporting visual presentations of formal specifications, so as to "make the best of both formal and informal worlds". Although we developed this method for the (logical-algebraic) specification languages CASL and CASL-LTL, we believe it is general enough to be adapted to other paradigms.
Another challenge is that a method that is too general does not encompass the different kinds of systems to be studied, while too many different specialized methods and paradigms result in partial views that may be difficult to integrate in a single global one. We deal with this issue by providing a limited number of instances of our method, fitted for three different kinds of software items and two specification approaches, while keeping a common "meta"-structure and way of thinking. More precisely, we consider here that a software item may be a simple dynamic system, a structured dynamic system, or a data structure. We also support both property-oriented (axiomatic) and model-oriented (constructive) specifications. We are thus providing support for the "building-bricks" tasks of specifying/modelling software artifacts that in our experience are needed for the development process.
Our approach is illustrated with a lift case study, it was also used with other large case studies, and when used on projects by students yielded homogeneous results.
Let us note that it may be used either as itself, e.g., for requirements specification, or in combination with structuring concepts such as the Jackson's problem frames.
slides: http://www-lipn.univ-paris13.fr/~choppy/SLIDES/menorca-talk.ps, http://www-lipn.univ-paris13.fr/~choppy/SLIDES/menorca-talk.pdf
paper: http://www-lipn.univ-paris13.fr/~choppy/PAPERS/FGmethod-ChoppyReggio03.ps, http://www-lipn.univ-paris13.fr/~choppy/PAPERS/FGmethod-ChoppyReggio03.pdf, ftp://ftp.disi.unige.it/person/ReggioG/ChoppyReggio03a.pdf
Till MossakowskiFor the specification of large software systems, heterogeneous multi-logic specifications are needed, since complex problems have different aspects that are best specified in different logics. A combination of all the used logics would become too complex in many cases. Moreover, using heterogeneous specifications, different approaches being developed at different sites can be related, i.e. there is a formal interoperability among languages and tools. In many cases, specialized languages and tools have their strengths in particular aspects. Using heterogeneous specification, these strengths can be combined with comparably small effort.
BISS, Dept. of Computer Science, University of Bremen
The most prominent approach to heterogeneous specification is CafeOBJ with its cube of eight logics and twelve projections (formalized as institution morphisms) among them, and having a semantics based on Diaconescu's notion of Grothendieck institution. However, this approach has a limitation: only one type of translation between institution is used, namely institution morphisms. Tarlecki is more general, he introduces a whole bunch of heterogeneous constructs for different kinds of translations. However, only one kind of translation can be used at a time. The goal of the present work is to overcome these limitations while simultaneously staying as simple as possible.
We provide a semantic basis for heterogeneous specifications that not only involve different logics, but also different kinds of translations between these. We show that Grothendieck institutions based on spans of (co)morphisms can serve as a unifying framework providing a simple but powerful semantics for heterogeneous specification. This is illustrated with an example heterogeneous specification involving first-order logic, the process algebra CSP and CTL (computational tree logic).
slides: http://www.tzi.de/~till/papers/ifip03.pdf
paper: http://www.tzi.de/~till/publications.html#hetspec
Kokichi FutatsugiCafeOBJ is a formal specification language equipped with verification methodologies based on algebraic specification technique. CafeOBJ is an executable wide spectrum language based on multiple logical foundations; mainly based on initial and hidden algebra. Static aspects of systems are specified in terms of initial algebra, and dynamic aspects of systems are specified in terms of hidden algebra.
Chair of Language Design, Graduate School of Information Science
Japan Advanced Institute of Science and Technology, JAPAN
e-mail: kokichi@jaist.ac.jp, web: http://www.jaist.ac.jp/~kokichi
CafeOBJ is the first algebraic specification language which incorporates observational (or behavioral) specifications based on hidden algebra in a serious way. Observational specifications in CafeOBJ can be seen as a nice combination of static and dynamic specifications, and facilitate natural and transparent specification and verification of complex systems.
The talk gives a progress report of recent development around CafeOBJ language system and formal methods based on it; especially, it mainly explains how to write proof scores in CafeOBJ for inductive proofs of initial and behavioral/observational specifications.
Home page of CafeOBJ:
http://www.ldl.jaist.ac.jp/cafeobj
Grigore RosuOrdinary software engineers and programmers can understand easily regular patterns, as shown by the immense interest in and the success of scripting languages like Perl, based essentially on regular expression pattern matching. We believe that regular expressions provide an elegant and powerful specification language also for monitoring requirements, because an execution trace of a program is in fact a string of states. Extended regular expressions (EREs) add complementation to regular expressions, which brings additional benefits by allowing one to specify patterns that must *not* occur during an execution. Complementation gives one the power to express patterns on strings non-elementarily more compactly. In this paper we present a technique to generate *optimal monitors* from EREs. Our monitors are deterministic finite automata (DFA) and our novel contribution is to generate them using *coinduction*. Based on experiments with our implementation, which can be publicly tested and used over the web, we believe that our technique is more efficient than the simplistic method based on complementation of automata which can quickly lead to a highly-exponential state explosion.
Department of Computer Science, University of Illinois at Urbana-Champaign, USA
slides: Meeting-2003-Menorca-Rosu.ppt
Carolyn Talcott, SRI InternationalIn a distributed system, a remote service framework must provide mechanisms for service publication and discovery, and for interacting with remote services. In addition there should be support for a variety of security properties: protecting information communicated between client and server, assuring client and server of each others identity, and enforcing access policies. The latter should be largely transparent to the client and service applications. To address these requirements, the Secure Service Proxy Toolkit (SSPTK), was developed by John Mitchell, Ninghui Li, and Derrick Tong at Stanford, based on Java RMI and Jini technologies. The objective of the work reported herein was to formally model and analyze the SSPTK using Maude (http://maude.cs.uiuc.edu). The formal models developed provided clear documentation of the design, and refined it to provide security protection tuned to against different types of attack. In the process of modeling and analysis a security hole was found in the design (and implementation) that was subsequently fixed. To analyze these models, models of attackers with different capabilities were developed. Properties of interest, for example success of different attacks, were modeled as as patterns such that a system state satisfies the property if it matches the pattern. Analysis resulted in tables documenting which attacks succeed or fail for toolkits providing given security levels. The code and analyses will be available at http://www-formal.stanford.edu/clt/FTN/SPTK/
Slides from WG1.3 presentation June 2003, Menorca are available as [PPT], [PDF]
The aim of the project MMiSS (Multi-Media Instruction in Safe and Secure Systems), funded by the German Ministry of Education and Research (BMBF), is the construction of a multi-media Internet-based adaptive educational system. Its content will initially cover a curriculum in the area of Safe and Secure Systems. Traditional teaching materials (slides, handouts, annotated course material, assignments and so on) are to be converted into a new hypermedia format, integrated with tool interactions for formally developing correct software. To ensure "sustainable development", i.e. continuous long-term usability of the contents, coherence and consistency are especially emphasised, through extensive semantic linking of teaching elements and a particular version, configuration and change management, based on experience in formal software development and associated support tools, in particular CASL and the CATS and MAYA tool set.
The long-term goal is to offer an open-source platform to
URL of the slides: http://www.mmiss.de/papers/MMiSS-IFIP.pdf
Hubert BaumeisterIn this presentation I propose to use programming languages, like Java, to build executable models for software systems instead of using a modeling language like UML. The basic conjecture is that modern high-level programming languages have the abstraction mechanisms needed to express abstract designs of software systems without having to present the complete implementation of the final system first. Properties of these models can be expressed by formal specifications and automated tests. Reverse-engineering tools, like Together, may be used to present the Java program using a graphical notation like UML.
Institut für Informatik, Universität München (LMU)
The claim is exemplified by providing three different models of a Multi User Dungeon Game playable with different players using their mobile phones. The first model is a Java program modeling the basic rules of the MUD game. The second model extends the first model by introducing a model of mobility, i.e., how the software components move between the game server and the mobile phones of the participating players. In this model, mobility is simulated; all locations are simulated as objects running on the same Java Virtual Machine (JVM). Finally, the third model presents an implementation of real mobility, i.e., the components run and migrate to and from different JVMs.
The development process used to generate these models is Property Driven Development (PDD) introduced in this presentation. Each modeling step is driven by presenting tests (either using the Fit acceptance test framework or the JUnit unit test framework) and formal specifications in the Java Modeling Language (JML) motivated by the tests.
The PDD approach is similar to the Test Driven Development approach used in Extreme Programming; the difference is the use of JML specifications in the process and that the target of the process are models instead of final implementations.
slides: http://www.informatik.uni-muenchen.de/~baumeist/slides/ifip03.pdf
M. Bettaz, M. MaoucheThe paper reports on an attempt of introducing explicit mobility into Z notation. It comes at a time where research on formal models for mobility is still in its formative stages, and our contribution may be seen as a starting point for introducing new ideas in the domain. In the first part of the paper we show how to extend Z notation with a location attribute whose change in value is used to represent motion. In the second part of the paper we revisit a case study from the literature showing the benefits of the mobility framework we incorporated to Z. The formal semantics of our "Mobile Z" may be merely derived from the semantics of Z by bringing back the notion of location to that of state variable in Z notation. Keywords and phrases: Mobile computing, wireless networking, models for mobility, Z notation, Mobile Z, location, motion and explicit mobility.
Faculty of Information Technology
Philadelphia University, Jordan
bettaz@philadelphia.edu.jo, maouch@philadelphia.edu.jo
Pointer to the paper:
http://www.philadelphia.edu.jo/science/pdf/betazmob.pdf
| | | Abstracts of Talks |