«Syspect»

Publications (Source)

On this page:

 

go next top of page

1 Publications (Source)




@ARTICLE{FLO+2011,
  AUTHOR = {Johannes Faber and Sven Linker and Ernst-R{\"u}diger Olderog and
	Jan-David Quesel},
  TITLE = {Syspect - Modelling, Specifying, and Verifying Real-Time Systems with
	Rich Data},
  JOURNAL = {International Journal of Software and Informatics},
  YEAR = {2011},
  VOLUME = {5},
  NUMBER = {1-2},
  PART = {1},
  PAGES = {117--137},
  NOTE = {ISSN 1673-7288.},
  URL = {http://www.ijsi.org/IJSI/ch/reader/create_pdf.aspx?file_no=i78&flag=1&journal_id=ijsi},
  ABSTRACT = {We introduce the graphical tool Syspect for modelling, specifying,
                  and automatically verifying reactive systems with continuous
                  real-time constraints and complex, possibly infinite data. For
                  modelling these systems, a UML profile comprising component
                  diagrams, protocol state machines, and class diagrams is used;
                  for specifying the formal semantics of these models, the
                  combination CSP-OZ-DC of CSP (Communicating Sequential
                  Processes), OZ (Object-Z) and DC (Duration Calculus) is
                  employed; for verifying properties of these specifications,
                  translators are provided to the input formats of the model
                  checkers ARMC (Abstraction Refinement Model Checker) and SLAB
                  (Slicing Abstraction model checker) as well as the tool
                  H-PILoT (Hierarchical Proving by Instantiation in Local Theory
                  extensions). The application of the tool is illustrated by a
                  selection of examples that have been successfully analysed
                  with Syspect. },
}


@TECHREPORT{FIJS2010,
  AUTHOR = {Johannes Faber and Carsten Ihlemann and Swen Jacobs and Viorica Sofronie-Stokkermans},
  TITLE = {Automatic Verification of Parametric Specifications with Complex
	Topologies},
  INSTITUTION = {SFB/TR 14 AVACS},
  YEAR = {2010},
  TYPE = {Reports of SFB/TR 14 AVACS},
  NUMBER = {66},
  NOTE = {ISSN: 1860-9821, \url{http://www.avacs.org}{http://www.avacs.org}.},
  ABSTRACT = {The focus of this paper is on reducing the complexity in verification
	by exploiting modularity at various levels: in specification, in
	verification, and structurally. For specifications, we use the modular
	language CSP-OZ-DC, which allows us to decouple verification tasks
	concerning data from those concerning durations. At the verification
	level, we exploit modularity in theorem proving for rich data structures
	and use this for invariant checking. At the structural level, we
	analyze possibilities for modular verification of systems consisting
	of various components which interact. We illustrate these ideas by
	automatically verifying safety properties of a case study from the
	European Train Control System standard, which extends previous examples
	by comprising a complex track topology with lists of track segments
	and trains with different routes.},
  ACCESS = {open},
  BIBTEX = {atr066.bib},
  EDITOR = {Bernd Becker and Werner Damm and Martin Fr{\"a}nzle and Ernst-R{\"u}diger
	Olderog and Andreas Podelski and Reinhard Wilhelm},
  SERIES = {ATR},
  SUBPROJECT = {R1},
  URL = {http://csd.informatik.uni-oldenburg.de/~jfaber/dl/ATR066.pdf},
}


@ARTICLE{MORW08,
  AUTHOR = {M. M{\"o}ller and E.-R. Olderog and H. Rasch and H.
                 Wehrheim},
  TITLE = {Integrating a Formal Method into a Software
                 Engineering Process with {UML} and {Java}},
  JOURNAL = {Formal Apsects of Computing},
  YEAR = {2008},
  VOLUME = {20},
  PAGES = {161--204},
  ABSTRACT = {We describe how CSP-OZ, a formal method combining the
                 process algebra CSP with the specification language
                 Object-Z, can be integrated into an object-oriented
                 software engineering process employing the UML as a
                 modelling and Java as an implementation language. The
                 benefit of this integration lies in the rigour of the
                 formal method, which improves the precision of the
                 constructed models and opens up the possibility of (1)
                 verifying properties of models in the early design
                 phases, and (2) checking adherence of implementations
                 to models. The envisaged application area of our
                 approach is the design of distributed {\em reactive
                 systems}. To this end, we propose a specific UML {\em
                 profile} for reactive systems. The profile contains
                 facilities for modelling components, their interfaces
                 and interconnections via synchronous/broadcast
                 communication, and the overall architecture of a
                 system. The integration with the formal method proceeds
                 by generating a significant part of the CSP-OZ
                 specification from the initially developed UML model.
                 The formal specification is on the one hand the
                 starting point for {\em verifying} properties of the
                 model, for instance by using the FDR model checker. On
                 the other hand, it is the basis for generating {\em
                 contracts} for the final implementation. Contracts are
                 written in the Java Modeling Language (JML)
                 complemented by \CSPjassda{}, an assertion language for
                 specifying orderings between method invocations. A set
                 of tools for runtime checking can be used to supervise
                 the adherence of the final Java implementation to the
                 generated contracts.},
}


@ARTICLE{Meyer2008,
  AUTHOR = {R. Meyer and J. Faber and J. Hoenicke and A. Rybalchenko},
  TITLE = {Model Checking Duration Calculus: A Practical Approach},
  JOURNAL = {Formal Aspects of Computing},
  YEAR = {2008},
  PUBLISHER = {Springer London},
  VOLUME = {20},
  PAGES = {481--505},
  NUMBER = {4--5},
  MONTH = JUL,
  NOTE = {{ISSN} 0934-5043 (Print) 1433-299X (Online)},
  ABSTRACT = {Model checking of real-time systems against Duration Calculus (DC)
	specifications requires the translation of DC formulae into automata-based
	semantics. The existing algorithms provide a limited DC coverage
	and do not support compositional verification. We propose a translation
	algorithm that advances the applicability of model checking tools
	to realistic applications. Our algorithm significantly extends the
	subset of DC that can be checked automatically. The central part
	of the algorithm is the automatic decomposition of DC specifications
	into sub-properties that can be verified independently. The decomposition
	is based on a novel distributive law for DC. We implemented the algorithm
	in a tool chain for the automated verification of systems comprising
	data, communication, and real-time aspects. We applied the tool chain
	to verify safety properties in an industrial case study from the
	European Train Control System (ETCS).},
  DOI = {10.1007/s00165-008-0082-7},
  ISSN = {0934-5043},
  KEYWORDS = {Model checking, Verification, Duration Calculus, Timed automata, Real-time
	systems, European Train Control System, Case study},
  URL = {http://www.springerlink.com/content/81g876074077601g/fulltext.pdf},
}

 top of page go back