Maritta Heisel

Prof. Dr. Maritta Heisel
Raum BB 919
Tel. : +49 203 379 3465
Fax : +49 379 4490
E-Mail : maritta.heisel[at]uni-duisburg-essen.de

Research
  • Compliance [Veröffentlichungen]
  • Formal Methods
    Veröffentlichungen:

    QuickSearch:   Number of matching entries: 0.

    YearTitleAuthorJournal/ProceedingsPublisher
    2008 A Formal Metamodel for Problem Frames Hatebur, D., Heisel, M. & Schmidt, H. Proceedings of the International Conference on Model Driven Engineering Languages and Systems (MODELS)    
    Abstract: Problem frames are patterns for analyzing, structuring, and characterizing
    software development problems. This paper presents a formal metamodel
    for problem frames expressed in UML class diagrams and using the formal specification
    notation OCL. That metamodel clarifies the nature of the different syntactical
    elements of problem frames, as well as the relations between them. It
    provides a framework for syntactical analysis and semantic validation of newly
    defined problem frames, and it prepares the ground for tool support for the problem
    frame approach.
    BibTeX:
    @techreport{HHS2008,
      year = {2008},
      title = {A Formal Metamodel for Problem Frames},
      booktitle = {Proceedings of the International Conference on Model Driven Engineering Languages and Systems (MODELS)},
      author = {Hatebur, Denis and Heisel, Maritta and Schmidt, Holger},
      series = {LNCS 5301},
      pages = {68--82},
      url = {https://link.springer.com/}
    }
    
    2007 Enhancing Dependability of Component-Based Systems Lanoix, A., Hatebur, D., Heisel, M. & Souquières, J. Reliable Software Technologies -- Ada Europe 2007   Springer  
    Abstract: We present an approach for enhancing dependability of component-
    based software. Functionality related to security, safety and reliability
    is encapsulated in specific components, allowing the method to
    be applied to off-the-shelf components. Any set of components can be
    extended with dependability features by wrapping them with special
    components, which monitor and filter input and outputs. This approach
    is supported by a rigorous development methodology based on UML and
    the B method and is introduced on the level of software architecture.
    BibTeX:
    @inproceedings{LHH+2007,
      year = {2007},
      title = {Enhancing Dependability of Component-Based Systems},
      booktitle = {Reliable Software Technologies -- Ada Europe 2007},
      author = {Lanoix, Arnaud and Hatebur, Denis and Heisel, Maritta and Souqui{\`{e}}res, Jeanine},
      publisher = {Springer},
      series = {LNCS 4498},
      pages = {41--54},
      url = {https://link.springer.com/}
    }
    
    2006 Proving Component Interoperability with B Refinement Chouali, S., Heisel, M. & Souquières, J. Electronic Notes in Theoretical Computer Science    
    BibTeX:
    @article{CHS2006,
      year = {2006},
      title = {Proving Component Interoperability with B Refinement},
      author = {Chouali, Samir and Heisel, Maritta and Souqui{\`{e}}res, Jeanine},
      journal = {Electronic Notes in Theoretical Computer Science},
      volume = {160},
      pages = {157--172}
    }
    
    2005 Proving Component Interoperability with B Refinement Chouali, S., Heisel, M. & Souquières, J. International Workshop on Formal Aspects on Component Software    
    Abstract: We use the formal method B for specifying interfaces of software components. Each component interface is equipped with a suitable data model defining all types occurring in the signature of interface operations. Moreover, pre- and postconditions have to be given for all interface operations. The interoperability between two components is proved by using a refinement relation between an adaption of the interface specifications.
    BibTeX:
    @inproceedings{ChoualiHeiselSouquieres05,
      year = {2005},
      title = {Proving Component Interoperability with {B} Refinement},
      booktitle = {{International Workshop on Formal Aspects on Component Software}},
      author = {Chouali, Samir and Heisel, Maritta and Souqui{\`{e}}res, Jeanine},
      publisher = {CSREA Press},
      pages = {915-920}
    }
    
    2003 Use of Patterns in Formal Development: Systematic Transition From Problems to Architectural Designs Choppy, C. & Heisel, M. Recent Trends in Algebraic Development Techniques, 16th WADT, Selected Papers   Springer  
    Abstract: We present a pattern-based software lifecycle and a method that supports the systematic execution of that lifecycle. First, problem frames are used to develop a formal specification of the problem to be solved. In a second phase, architectural styles are used to construct an architectural specification of the software system to be developed. That specification forms the basis for fine-grained design and implementation.
    BibTeX:
    @inproceedings{CH2003,
      year = {2003},
      title = {Use of Patterns in Formal Development: Systematic Transition From Problems to Architectural Designs},
      booktitle = {Recent Trends in Algebraic Development Techniques, 16th WADT, Selected Papers},
      author = {Choppy, Christine and Heisel, Maritta},
      publisher = {Springer},
      series = {LNCS 2755},
      pages = {205--220},
      url = {https://link.springer.com/}
    }
    
    2003 Formalisation des besoins à l`aide de schémas LSCs Souquières, J. & Heisel, M. Proceedings Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL'2003    
    Abstract: Dans notre approche pour l'expression des besoins, nous proposons d'intégrer une
    étape de formalisation très tôt dans le développement an d'analyser de manière détaillée les besoins
    des utilisateurs et de découvrir les inconsistances et les problèmes à partir des difcultés
    rencontrées lors de la formalisation. An d'améliorer la lisibilité et l'écriture des besoins formalis
    és, nous proposons d'utiliser les LSCs, Life Sequence Charts, au lieu des formules pour la
    formalisation des besoins décomposés sous forme de fragments. Nous proposons, en particulier,
    des schémas graphiques pour exprimer différents types de besoins. Ces schémas constituent un
    guide à la formalisation.
    BibTeX:
    @inproceedings{SH2003,
      year = {2003},
      title = {Formalisation des besoins {\`{a}} l`aide de sch{\'{e}}mas {LSCs}},
      booktitle = {Proceedings Approches Formelles dans l'Assistance au D{\'{e}}veloppement de Logiciels - AFADL'2003},
      author = {Souqui{\`{e}}res, Jeanine and Heisel, Maritta},
      pages = {53--63},
      note = {ISBN 2-7261-1236-6}
    }
    
    2002 Logische Modellierung von Anwendungswelten aus Benutzersicht Heisel, M. & Krömker, H. Workshop Proceedings "Multimediale Informations- und Kommunikationssysteme, NET.OBJECT Days 2002"    
    Abstract: Der Softwareentwicklung fehlt oft eine detaillierte methodische Unterstützung von technischen Softwareentwicklungsaktivitäten. Eine Autorin dieses Papiers hat das Konzept der Agenda entwickelt, das zum Ziel hat, Softwareentwicklungswissen als "methodische Essenzen" von Softwareentwicklungsaktivitäten explizit zu repräsentieren. Zur logischen Modellierung von Anwendungswelten aus Benutzersicht wird eine Agenda entwickelt, die es erlaubt diese Anwendungswelt methodisch in Konzepten der Handlungspsychologie zu erheben.
    BibTeX:
    @inproceedings{Heisel2002,
      year = {2002},
      title = {Logische Modellierung von Anwendungswelten aus Benutzersicht},
      booktitle = {Workshop Proceedings "Multimediale Informations- und Kommunikationssysteme, NET.OBJECT Days 2002"},
      author = {Heisel, Maritta and Kr{\"{o}}mker, Heidi},
      publisher = {tranSIT GmbH, Ilmenau},
      pages = {649--656},
      note = {ISBN 3-9808628-1-X}
    }
    
    2002 Toward a formal model of software components Heisel, M., Santen, T. & Souquières, J. Proc. 4th International Conference on Formal Engineering Methods   Springer  
    Abstract: We are interested in specifying component models in a way that allows
    us to analyze the interplay of components in general, and to concisely specify
    individual components. As a starting point for coming up with a technique of
    specifying component models, we consider JavaBeans. We capture the JavaBean
    component model using UML class diagrams, Object-Z, and life sequence charts.
    BibTeX:
    @inproceedings{HSS2002,
      year = {2002},
      title = {Toward a formal model of software components},
      booktitle = {Proc.\ 4th International Conference on Formal Engineering Methods},
      author = {Heisel, Maritta and Santen, Thomas and Souqui{\`{e}}res, Jeanine},
      publisher = {Springer},
      series = {LNCS 2495},
      pages = {57--68},
      url = {https://link.springer.com/}
    }
    
    2002 Confidentiality-Preserving Refinement is Compositional -- Sometimes Santen, T., Heisel, M. & Pfitzmann, A. Proc. Computer Security -- ESORICS 2002   Springer  
    Abstract: Confidentiality-preserving refinement describes a relation between a
    specification and an implementation that ensures that all confidentiality properties
    required in the specification are preserved by the implementation in a probabilistic
    setting. The present paper investigates the condition under which that notion
    of refinement is compositional, i.e. the condition under which refining a subsystem
    of a larger system yields a confidentiality-preserving refinement of the larger
    system. It turns out that the refinement relation is not composition in general,
    but the condition for compositionality can be stated in a way that builds on the
    analysis of subsystems thus aiding system designers in analyzing a composition.
    BibTeX:
    @inproceedings{SHP2002,
      year = {2002},
      title = {Confidentiality-Preserving Refinement is Compositional -- Sometimes},
      booktitle = {Proc.\ Computer Security -- ESORICS 2002},
      author = {Santen, Thomas and Heisel, Maritta and Pfitzmann, Andreas},
      publisher = {Springer},
      series = {LNCS 2502},
      pages = {194--211},
      url = {https://link.springer.com/}
    }
    
    2002 Specification and Refinement of Secure IT Systems Santen, T., Pfitzmann, A. & Heisel, M. Proc. International Workshop on Refinement of Critical Systems    
    BibTeX:
    @inproceedings{SPH2002,
      year = {2002},
      title = {Specification and Refinement of Secure {IT} Systems},
      booktitle = {Proc.\ International Workshop on Refinement of Critical Systems},
      author = {Santen, Thomas and Pfitzmann, Andreas and Heisel, Maritta},
      note = {http://www.esil.univ-mrs.fr/\verb|~|spc/rcs02/papers/Santen.ps.gz}
    }
    
    2001 Specifying Safety-Critical Embedded systems with Statecharts and Z: An Agenda for Cyclic Software Components Grieskamp, W., Heisel, M. & Dörr, H. Science of Computer Programming    
    Abstract: The application of formal techniques can contribute much to the quality of software, which is of utmost importance for safety-critical embedded systems. These techniques, however, are not easy to apply. In particular, methodological guidance is often unsatisfactory. We address this problem by the concept of an agenda. An agenda is a list of activities to be performed for solving a task in software engineering. Agendas used to support the application of formal specification techniques provide detailed guidance for specifiers, templates of the used specification language that only need to be instantiated, and application independent validation criteria. We apply the agenda approach to a particular class of embedded safety-critical systems, the formal specification of which has been investigated in the case-studies of the German Espress project during the last two years.
    BibTeX:
    @article{Grieskamp2001,
      year = {2001},
      title = {Specifying Safety-Critical Embedded systems with {S}tatecharts and {Z}: An Agenda for Cyclic Software Components},
      author = {Grieskamp, Wolfgang and Heisel, Maritta and D{\"{o}}rr, Heiko},
      journal = {Science of Computer Programming},
      volume = {40},
      pages = {31--57}
    }
    
    2001 Confidentiality-Preserving Refinement Heisel, M., Pfitzmann, A. & Santen, T. Proc. 14th IEEE Computer Security Foundations Workshop    
    Abstract: We develop a condition for confidentiality-preserving refinement which is both necessary and sufficient. Using a slight extension of CSP as notation, we give a toy example to illustrate the usefulness of our condition.
    Systems are specified by their behavior and a window. For an abstract system, the window specifies what information is allowed to be observed by its environment. For a concrete system, the window specifies what information cannot be hidden from its environment. A concrete system is a confidentiality-preserving refinement of an abstract system,
    if it behaviorally refines the abstract system and if the
    information revealed by the concrete window is allowed to
    be revealed according to the abstract window.
    BibTeX:
    @inproceedings{HPS2001,
      year = {2001},
      title = {Confidentiality-Preserving Refinement},
      booktitle = {Proc.\ 14th IEEE Computer Security Foundations Workshop},
      author = {Heisel, Maritta and Pfitzmann, Andreas and Santen, Thomas},
      publisher = {IEEE Computer Society},
      pages = {295--305}
    }
    

    Created by JabRef on 13/03/2018.

  • Methodology [Veröffentlichungen]
  • Patterns [Veröffentlichungen]
  • Privacy [Veröffentlichungen]
  • Requirements Engineering [Veröffentlichungen]
  • Safety [Veröffentlichungen]
  • Security [Veröffentlichungen]
  • Software Architecture [Veröffentlichungen]
  • Software Quality [Veröffentlichungen]
  • Test [Veröffentlichungen]