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

The Conference for Software Architecture
Munich, 05 February - 09 February 2018


Talk: Di 2.2
Date: Tue, 06.02.2018
Time: 14:00 - 14:45

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

Time: 14:00 - 14:45
Talk: 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 Gold Sponsor
  • Atlassian Gold Sponsor
  • German Testing Board e.V. Gold Sponsor
  • Intel Software Gold Sponsor
  • Volkswagen Gold Sponsor
  • andrena objects ag Silver Sponsor
  • AppDynamics Silver Sponsor
  • IBM Deutschland GmbH Silver Sponsor
  • ITech Progress GmbH Silver Sponsor
  • Microsoft Deutschland GmbH Silver Sponsor
  • Ab Initio Software Germany GmbH Bronze Sponsor
  • adesso AG Bronze Sponsor
  • agile42 GmbH Bronze Sponsor
  • Axway GmbH Bronze Sponsor
  • Capgemini Bronze Sponsor
  • DEUTSCHE TELEKOM AG Bronze Sponsor
  • innoQ Deutschland GmbH Bronze Sponsor
  • iteratec GmbH Bronze Sponsor
  • New Relic Bronze Sponsor
  • Novatec Consulting GmbH Bronze Sponsor
  • OPEN KNOWLEDGE GmbH Bronze Sponsor
  • OPITZ CONSULTING GmbH Bronze Sponsor
  • Servicetrace GmbH Bronze Sponsor
  • ThoughtWorks Deutschland GmbH Bronze Sponsor
  • XebiaLabs Bronze Sponsor
  • AI Spektrum Partner
  • Bitkom e.V. Partner
  • Business Application Research Center - BARC GmbH Partner
  • JavaSPEKTRUM Partner
  • OBJEKTspektrum Partner
  • TDWI e.V. Partner