Séminaires
Séminaire du 18 Mars 2005
Lieu
Programme
14h00-15h00: Berndt Farwer, Université de Hamburg (Germany): Separation of control flow and data flow in high-level Petri nets. (Towards readability and verification of complex systems.)
Abstract: the presentation shows how the idea of control/data separation can be modelled with object Petri nets. We summarise a translation from Dual Flow Nets (DFNs) to Object-Based Petri Nets (OPNs). The motivation for this work is that verification of large-scale systems is too complex for many practical applications, but there are also many fields in which a complete verification is not necessary. It pays to separate control flow from data flow, since we can then more easily verify the parts of the system that are most important for the application, thus giving rise to a reduction of the overall complexity. With OPNs it will then be easy to find a suitable level of abstraction of the data to the respective needs of the modelled system by introducing further nesting of parts of the data.
15h00-16h00 : Christine Choppy, Université Paris Nord, laboratoire LIPN joint work with Gianna Reggio Formally grounded requirement specification methodology
Abstract: 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 notations) 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 when writing a specification. Our approach aims at helping to produce adequate requirements, both clear and precise enough so as to provide a sound basis to the overall development, and to provide a companion method that helps the user to understand the system to be developed, and to write the corresponding formal specifications. We present a technique for improving use case based requirements, by producing a companion Formally Grounded specification, that results both in an improved requirements capture, and in a requirement validation. The Formally Grounded requirements specification is written in a ``visual'' notation, using both diagrams and text, with a formal counterpart (written in the CASL and CASL-LTL languages). The resulting use case based requirements are of high quality, more systematic, more precise, and its corresponding Formally Grounded specification is available. We illustrate our approach with a lift case study and an Auction System case study.