Hinweis: Die aktuelle OOP-Konferenz finden Sie hier!
SIGS DATACOM Fachinformationen für IT-Professionals

Die Konferenz für Software-Architektur
05. - 09. Februar 2018, München


Vortrag: Di 2.2
Datum: Di, 06.02.2018
Uhrzeit: 14:00 - 14:45

Experiences from Applying Formal Verification on the Siemens SIMATIC S7-400H Firmware Using SPIN

Uhrzeit: 14:00 - 14:45
Vortrag: Di 2.2


The presentation summarizes experiences in applying formal verification of software design artifacts using the SPIN model checker. The discussed example covers a crucial part of the firmware of the fault-tolerant programmable logic controller SIMATIC S7-400H. The presentation advocates the combination of formal verification of design artifacts with an appropriate test method applied on the software implementation. While formal verification complements the review process, testing benefits from the availability of correct formal models.

Target Audience: Software Engineers, Managers
Prerequisites: Experiences in software design and modeling languages; understanding of the V&V process
Level: Practicing

Extended Abstract
The development of a distributed system that comprises two or more components distributed over a network is challenging because of the inherent concurrency and need for coordination and synchronization. The problem is aggravated further if this system needs to fulfill stringent safety requirements. This presentation discusses an approach that is based on software behavior modeling and verifies the correctness of the model against the safety requirements. Afterwards this model is used to validate the correctness of the software implementation during testing. The approach is implemented using the open-source model-checker tool SPIN.
The presentation discusses the experiences in applying the outlined approach on a crucial part of the firmware of the fault-tolerant programmable logic controller Siemens SIMATIC S7-400H. It outlines the whole iterative process of model construction from available C code, model extension with new system features, model correctness checking using SPIN, validation of the C code implementation against the model via runtime verification during the testing phase. During the process design faults in the model and implementation faults in the running system are identified that would be hard to find using conventional methods of code review and testing.


Sponsoren der OOP 2018

  • Accenture Technology Solutions GmbH Goldsponsor
  • Atlassian Goldsponsor
  • German Testing Board e.V. Goldsponsor
  • Intel Software Goldsponsor
  • Volkswagen Goldsponsor
  • andrena objects ag Silbersponsor
  • AppDynamics Silbersponsor
  • IBM Deutschland GmbH Silbersponsor
  • ITech Progress GmbH Silbersponsor
  • Microsoft Deutschland GmbH Silbersponsor
  • Ab Initio Software Germany GmbH Bronzesponsor
  • adesso AG Bronzesponsor
  • agile42 GmbH Bronzesponsor
  • Axway GmbH Bronzesponsor
  • Capgemini Bronzesponsor
  • DEUTSCHE TELEKOM AG Bronzesponsor
  • innoQ Deutschland GmbH Bronzesponsor
  • iteratec GmbH Bronzesponsor
  • New Relic Bronzesponsor
  • Novatec Consulting GmbH Bronzesponsor
  • OPEN KNOWLEDGE GmbH Bronzesponsor
  • OPITZ CONSULTING GmbH Bronzesponsor
  • Servicetrace GmbH Bronzesponsor
  • ThoughtWorks Deutschland GmbH Bronzesponsor
  • XebiaLabs Bronzesponsor
  • AI Spektrum Partner
  • Bitkom e.V. Partner
  • Business Application Research Center - BARC GmbH Partner
  • JavaSPEKTRUM Partner
  • OBJEKTspektrum Partner
  • TDWI e.V. Partner