Zuviel Werbung? - > Hier kostenlos beim SPS-Forum registrieren

Seite 1 von 5 123 ... LetzteLetzte
Ergebnis 1 bis 10 von 48

Thema: Umfrage: Formale Verifikation / Modellprüfung

  1. #1
    Registriert seit
    15.04.2014
    Beiträge
    10
    Danke
    6
    Erhielt 4 Danke für 4 Beiträge

    Frage


    Zuviel Werbung?
    -> Hier kostenlos registrieren
    Hallo Leute,

    ich bin kürzlich mal zufällig auf das Thema Formale Verifikation von Programmen gestoßen und mir kommt das Konzept - grade im Bereich Automatisierungstechnik - extrem hilfreich vor und es ist mir ein Rätsel, warum ich davon jetzt zum ersten mal höre. Nachdem ich aber selbst in meiner Berufslaufbahn bisher vergleichsweise selten zum tatsächlichen SPS-Programmieren gekommen bin, wollte ich hier ein wenig "Marktforschung" betreiben bei den Leuten, die drin sind in der Materie.



    Zunächst für alle die's nicht wissen: Was ist Model Checking?
    Ein großes Problem beim Programmieren ist ja die Fehlersuche. Normalerweise mache ich dabei im Prinzip folgendes:
    Normaler Testablauf:

    1. Ich überlege mir, welche Betriebsfälle eintreten können. Insbesondere welche einen Fehler hervorrufen könnten.
    2. Ich teste die Fälle und prüfe, ob das eintretende Verhalten das gewünschte ist.
    3. Wenn ja -> gut, wenn nein -> Fehler beheben.

    Das ganze kann ich strukturiert machen (z.B. Unit Testing) oder manuell, indem ich, auf gut Deutsch gesagt, solang rumprobiere bis alles geht.

    Problematisch ist der erste Schritt, denn durch Überlegung kommt man kaum auf alle abstrusen Fehler, die sich so in ein Programm einschleichen. Jeder der mal irgendwas programmiert hat kennt das Problem.

    Bei der Modellprüfung funktioniert der Ablauf deshalb so:
    1. Ich lege eine Reihe von Bedingungen fest, die IMMER vom Programm eingehalten werden. z.B. "Niemals NOT-Aus und Motor an", "Niemals A0.1 für länger als 10 Sekunden", "Wenn sqrt(EW5 * EW6 > 10) dann irgendwann A0.5 = 1 binnen 8s". Alle Bedingungen zusammen ergeben das sog. Modell.
    2. Der Model Checker prüft JEDEN MÖGLICHEN BETRIEBSFALL des Programms auf die Wahrheit des Modells.
    3. Wenn kein Fall existiert, in dem das Modell nicht eingehalten wird -> gut, ansonsten -> fehlerhaftes Gegenbeispiel anzeigen -> Fehler beheben.


    In der Hardwareentwicklung ist diese Methodik der Formalen Verifikation recht verbreitet, z.B. um die korrekte Funktionsweise von Prozessoren zu beweisen. In der Softwareentwicklung habe zumindest ich noch nie etwas davon mitbekommen. Und bei SPS erst recht nicht.

    Eine Recherche ergab dann auch nicht arg viel. Ein Programm namens ArcadePLC hab ich gefunden:
    http://arcade.embedded.rwth-aachen.d...?id=arcade.plc
    Ist mir aber beim Datei laden abgestürzt, drum kann ich nichts dazu sagen. Bis auf eine kostenpflichtige Publikation des Entwicklers habe ich auch bei google keinerlei Dokumentation oder Diskussion dazu gefunden.

    Das Tool UPPAAL scheint relativ verbreitet zu sein, ist aber nicht speziell für SPSen gedacht : http://www.uppaal.com/index.php?sida=186&rubrik=93

    Ich habe nichts gefunden, wo ich einfach mein Programm/Projekt laden konnte, Bedingungen eingebe und dann ein Ergebnis erhalte.



    Jetzt zu meinem eigentlichen Anliegen:
    • Wem war das Prinzip schon vorher geläufig? Setzt ihr es ein?
    • Wenn ja: Welche Tools verwendet ihr dafür?
    • Wenn nein: Warum nicht?
    • Wer das Prinzip vorher nicht kannte: Was meint ihr dazu? Würdet ihr es einsetzen, wenn es eine gute Software dafür gäbe?
    • usw.


    Schonmal danke für die Antworten!
    Zitieren Zitieren Umfrage: Formale Verifikation / Modellprüfung  

  2. #2
    Registriert seit
    03.04.2008
    Beiträge
    6.200
    Danke
    237
    Erhielt 815 Danke für 689 Beiträge

    Standard

    Das Thema hat inzwischen einen echt langen Bart.
    Das Problem liegt daran, ein Modell zu erstellen.
    Bei einer Serie ab x + 1000 Stück pro Jahr ist solch eine Modulbildung vielleicht sinnvoll.
    Doch wer baut so viele Produkte in Serie?
    Zu den Tools die Frage:
    Wo gibt es für unsere Umgebung irgend welche Tools?

    Junge von der Uni, so abstrakt zu fragen zeigt, dass du dich mit der Automatisierung, das unser Geschäft hier ist, nicht im geringsten beschäftigt hast.



    bike
    "Any fool can write code that a computer can understand.
    Good programmers write code that humans can understand."
    --Martin Fowler

  3. Folgender Benutzer sagt Danke zu bike für den nützlichen Beitrag:

    ducati (16.04.2014)

  4. #3
    Registriert seit
    30.08.2010
    Ort
    Östereich
    Beiträge
    1.458
    Danke
    502
    Erhielt 217 Danke für 192 Beiträge

    Standard

    Punkt 1. wird wohl fast jeder Programmierer im SPS Umfeld machen.
    2. wird bei der IBS realisiert und daraus ergibt sich Punkt 3.

    Was willst du uns sagen?
    Elektrotechnik und Elektronik funktioniert mit Rauch (Beweis: Tritt Rauch aus, funktioniert auch das Bauteil nicht mehr)

  5. Folgender Benutzer sagt Danke zu winnman für den nützlichen Beitrag:

    ducati (16.04.2014)

  6. #4
    Skrjiban ist offline Neuer Benutzer
    Themenstarter
    Registriert seit
    15.04.2014
    Beiträge
    10
    Danke
    6
    Erhielt 4 Danke für 4 Beiträge

    Standard

    Hm, hab ich mich so unklar ausgedrückt?

    Das Problem liegt daran, ein Modell zu erstellen.
    Bei einer Serie ab x + 1000 Stück pro Jahr ist solch eine Modulbildung vielleicht sinnvoll.
    Doch wer baut so viele Produkte in Serie?
    Reden wir aneinander vorbei? Mir kommt es so vor, als ob du von einem 3D-Modell sprichst. Darum gehts mir nicht. Mir geht es um eine Spezifikation für ein SPS-Programm. Anschließend will ich prüfen, ob das Programm diese Spezifikation auch einhält. Und das automatisch, mit einem Software-Tool (= http://de.wikipedia.org/wiki/Model_Checking )

    Punkt 1. wird wohl fast jeder Programmierer im SPS Umfeld machen.
    2. wird bei der IBS realisiert und daraus ergibt sich Punkt 3.
    Da komm ich jetzt nicht ganz mit. Auf welche Punkte beziehst du dich?

  7. #5
    Registriert seit
    01.10.2012
    Beiträge
    203
    Danke
    12
    Erhielt 56 Danke für 36 Beiträge

    Standard

    Also m.E. ist das was für akademische Denkspiele.

    Ich muß mir ja im Vorfeld meinen Programmablauf, Funktionen und die Sicherheit überlegen und irgendwie definieren. Dieses Konzept wird dann umgesetzt, in dem ich diese Vorgaben mit einer Programmiersprache in eine Logik übersetze. Wenn sowas ordentlich gemacht wird, sollten schonmal kaum gravierende Bugs auftreten und wenn ich das ganze ordentlich strukturiere lassen sich Fehler auch schnell finden und ach Änderungen leichter einpflegen, zBsp. doppelter Code ist einmal zuviel.
    Ist auch immer abhängig von der Komplexität der Aufgabe, aber die meiste Arbeit liegt eigentlich vor dem Programmieren und da werden oft die meisten Fehler gemacht.
    Geändert von Bapho (16.04.2014 um 08:06 Uhr)
    Nüchtern betrachtet war es besoffen besser.

  8. Folgender Benutzer sagt Danke zu Bapho für den nützlichen Beitrag:

    ducati (16.04.2014)

  9. #6
    Registriert seit
    03.04.2008
    Beiträge
    6.200
    Danke
    237
    Erhielt 815 Danke für 689 Beiträge

    Standard

    Zitat Zitat von Skrjiban Beitrag anzeigen
    Hm, hab ich mich so unklar ausgedrückt?



    Reden wir aneinander vorbei? Mir kommt es so vor, als ob du von einem 3D-Modell sprichst. Darum gehts mir nicht. Mir geht es um eine Spezifikation für ein SPS-Programm. Anschließend will ich prüfen, ob das Programm diese Spezifikation auch einhält. Und das automatisch, mit einem Software-Tool (= http://de.wikipedia.org/wiki/Model_Checking )



    Da komm ich jetzt nicht ganz mit. Auf welche Punkte beziehst du dich?
    Bestimmt nicht.
    Für die Definition der Logik braucht doch zuerst ein Modell, was die Maschine bzw Anlage tun soll.
    Mit dieser Definition könnte man die Anforderung an das PLC Programm definieren.
    Aber dein Unverständnis zeigt, dass du zuerst dich um die Grundlagen kümmern und verstehen sollst.


    bike
    "Any fool can write code that a computer can understand.
    Good programmers write code that humans can understand."
    --Martin Fowler

  10. #7
    Registriert seit
    09.08.2006
    Beiträge
    3.626
    Danke
    911
    Erhielt 656 Danke für 542 Beiträge

    Standard

    Hihi, da treffen sie wieder aufeinander

    Für die (SPS-) Automatisierung ist das wirklich alles Quatsch, da einfach zu aufwendig... (erstens von der Zeit und zweitens von den Kosten)

    In der Automobilindustrie (Fahrzeugentwicklung, nicht Fertigung) wird sowas aber schon eingesetzt. Ich hab da mal nen Vortrag gehört, der hat die Algorithmen von nem Schachcomputer verwendet und quasi den Softwaretest gegen das Fahrzeugsteuergerät antreten lassen...

    Aber das ist alles schon etwas her, daher habe ich jetzt aus dem Hut auch keine weiterführenden Links.

    Aber wie Bike schon sagt, bei Produktzahlen im 6 oder 7 stelligen Bereich mit entsprechenden Kosten für Rückrufaktionen und Imageschäden lohnt sich der Aufwand. In der SPS-Automatisierung mit Verwendung des identischen Programms zwischen vielleicht 1 und 100 mal macht solch ein Aufwand wenig Sinn... Zumal das ganze nicht trivilal für den Durchschnittsingenieur umsetzbar ist.

    Was man heute schon häufig macht, ist eine mehr oder weniger aufwändige Simulation der Maschine/Anlage im Büro aufzubauen, um die Software mit angebundener simulierter Hardware zu testen. Das ist aber schon nicht ganz simpel. Natürlich könnte man sich jetzt vorstellen, die Simulationssoftware noch um einen automatischen "Softwarefehlersuchalgorithmus" zu erweitern. Aber solange das nicht wirklich intuitiv zu bedienen ist, sehe ich da für die Praxis schwarz.

    Erschwerend kommt hinzu, dass die SPS-Software ja nicht alleine dasteht, es gibt noch die Visualisierung, welche mittlerweile eine sehr großen Umfang besitzt. Also müsste für einen automatisierten Softwaretest auch automatisch Eingaben in der Visu vorgenommen werden... und das ist schon schwieriger ohne die Visu selbst zu manipulieren...

    Zurück zur Praxis: Softwarefehler sind schön und gut, aber Sorgen sind auf der Baustelle ganz andere vorhanden. In der Regel Projektorganisatorischer Art. Oft erfährt man erst auf der Baustelle, welcher Sensor mit welchem Messbereich an welcher Stelle wirklich verbaut ist... Da nützt die beste Simulation im Vorfeld nichts, wenn die Realität ganz anders aussieht.

    Aber trotzdem macht ne Simulation Sinn, ist aber aufwändig (geschätzte zusätzliche 50-100% der SPS-Softwarezeit)

    Gruß und habt Euch alle lieb

    PS: eine Industriesteuerung, wie wir sie hier regelmäßig errichten hat nicht 10 Eingänge und 10 Ausgänge sondern mal locker >1000 Eingänge und >500 Ausgänge. Und das sind u.U. nur Teilanlagen von einer großen Produktionsanlage... Das ist das Problem mit dem Aufwand...

    PPS: und nein, das sind keine Kernkraftwerke, wo man den Aufwand vielleicht noch rechtfertigen könnte

    PPPS: wenn etwas in der Praxis nicht gemacht wird, liegt das meist nicht daran, dass alle anderen so doof und man selbst so schlau ist sondern es gibt gute Gründe dafür... abundzu findet man aber trotzdem ne Marktlücke. Oder man hat gut Verkäufer, die auch den letzten Scheiss an den Mann bringen.
    Geändert von ducati (16.04.2014 um 09:15 Uhr)

  11. Folgende 4 Benutzer sagen Danke zu ducati für den nützlichen Beitrag:

    Aventinus (16.04.2014),LT Smash (17.04.2014),Skrjiban (16.04.2014),winnman (16.04.2014)

  12. #8
    Registriert seit
    07.01.2014
    Beiträge
    36
    Danke
    16
    Erhielt 7 Danke für 6 Beiträge

    Standard

    Meiner Meinung macht die Prüfung nur Sinn wenn auch standardisierte Softwarekomponenten verwendet werden. Wird ein Programm von Hand neu gestrickt ist der Aufwand zu groß. Das Problem besteht wohl da drin das der Programmierer und Prüfer der selbe sein wird. Wenn dir bei der Programmierung bestimmte Konstalationen nicht auffallen, wirst du auch bei der Prüfung nicht da dran denken.

    Ein guter SWtest ist sehr wichtig. Beim normalen Automatikablauf sind Fehler auch schnell gefunden. Das Problem ist eher, wie reagiere ich bei Fehler xy. Ich teste bei der Inbetriebnahme jede Fehlermeldung und hake sie ab. Damit läßt sich oft noch der ein oder andere Fehler finden.

    Aber das Zauberwort heißt: Standardisierung. Ein Motorbaustein der z.B. über einen UDT Fehler ausspuckt und gekapselt ist muss normalerweise nicht mehr getestet werden. So kann viel Zeit gespart werden.

    Zu deinem Punkt fällt mir noch folgendes ein:
    http://www.freepatentsonline.com/DE102010005308.html
    Geändert von MrSpexx (16.04.2014 um 09:25 Uhr)
    "Schau auf zu den Sternen, hab acht auf die Gassen".

  13. Folgender Benutzer sagt Danke zu MrSpexx für den nützlichen Beitrag:

    Skrjiban (16.04.2014)

  14. #9
    Registriert seit
    09.08.2006
    Beiträge
    3.626
    Danke
    911
    Erhielt 656 Danke für 542 Beiträge

    Standard

    Zitat Zitat von MrSpexx Beitrag anzeigen
    Meiner Meinung macht die Prüfung nur Sinn wenn auch standardisierte Softwarekomponenten verwendet werden. Wird ein Programm von Hand neu gestrickt ist der Aufwand zu groß.
    ...
    Aber das Zauberwort heißt: Standardisierung. Ein Motorbaustein der z.B. über einen UDT Fehler ausspuckt und gekapselt ist muss normalerweise nicht mehr getestet werden. So kann viel Zeit gespart werden.
    Jo, da dieser Motorbaustein dann ja vielleicht auch 10000 mal verwendet wird, könnte solch ein Test dafür u.U. sinnvoll sein (bzw. nach jeder "kleinen" Änderung mal den Test pauschal drüber laufen lassen). Oder Siemens könnte solch einen Automatischen Softwaretest für seine PCS7-APL-Bibliothek verwenden... Also allgemein für Programmierer von Bibliotheken.

    Aber für ein komplettes SPS-Programm macht das alles keinen Sinn.

    Gruß.

  15. Folgender Benutzer sagt Danke zu ducati für den nützlichen Beitrag:

    winnman (16.04.2014)

  16. #10
    Skrjiban ist offline Neuer Benutzer
    Themenstarter
    Registriert seit
    15.04.2014
    Beiträge
    10
    Danke
    6
    Erhielt 4 Danke für 4 Beiträge

    Standard


    Zuviel Werbung?
    -> Hier kostenlos registrieren
    Erstmal Danke für die ausführlichen Antworten. Zumindest weiß ich jetzt schonmal, dass die Methodik definitiv nicht in der Praxis gemacht wird, zumindest nicht bei SPS-Programmen.

    wenn etwas in der Praxis nicht gemacht wird, liegt das meist nicht daran, dass alle anderen so doof und man selbst so schlau ist
    Hat ja auch niemand behauptet

    Ich muß mir ja im Vorfeld meinen Programmablauf, Funktionen und die Sicherheit überlegen und irgendwie definieren. Dieses Konzept wird dann umgesetzt, in dem ich diese Vorgaben mit einer Programmiersprache in eine Logik übersetze. Wenn sowas ordentlich gemacht wird, sollten schonmal kaum gravierende Bugs auftreten und wenn ich das ganze ordentlich strukturiere lassen sich Fehler auch schnell finden und ach Änderungen leichter einpflegen, zBsp. doppelter Code ist einmal zuviel.
    Ist auch immer abhängig von der Komplexität der Aufgabe, aber die meiste Arbeit liegt eigentlich vor dem Programmieren und da werden oft die meisten Fehler gemacht.
    Da stimme ich dir natürlich zu. Ich entwickle hauptberuflich PC-Software und auch da ist es meist so, dass eine gute Planung schwieriger als die tatsächliche Implementierung ist. Eine andere Wahrheit ist aber auch, dass sich a) nie alles vorher planen lässt, weil immer wieder Änderungen vorkommen und b) in der Praxis dann doch im Schnitt ein nicht unwesentlicher Teil der Zeit und des Geldes (ich glaube 40% des Budgets oder sowas, habs grad nicht mehr im Kopf) für Fehlersuche und Behebung draufgeht. Ich weiß natürlich nicht wie das in der professionellen Automatisierungsindustrie aussieht (deswegen frage ich euch ja) - ich würde mal auf "ähnlich" tippen.

    Ansonsten war der Konsens hier ja, dass so eine Modellbildung zu aufwändig wäre, als dass es sich lohnen würde. Es geht aber ja auch gar nicht darum, das Verhalten vom ganzen Programm im Detail zu spezifizieren. Das ist natürlich utopisch. Und ich will die Modellbildung auch gar nicht in die Planungsphase einbinden. Es geht nur darum, das Testen am Ende schneller und sicherer zu machen, indem ich die _essenziellen_ Verhaltensweisen der Steuerung prüfe.

    Minibeispiel: Letztens hab ich eine Torsteuerung mit Logo programmiert. Das Tor sollte abends zugehen und morgens wieder auf (mit Zeitumstellung) das Tor konnte man von außen per Zugangskarte oder per Funk öffnen, von innen über Bewegungsmelder. Dann ne Lichtschranke zur Sicherheit, die verhindert dass jemand eingeklemmt wird. Ganz simpel. Nach ein bisschen rumprobieren lief das Ganze dann auch und die Tests waren gut. Ich bin nach Hause gefahren und hab am nächsten Tag erfahren dass das Tor natürlich nicht abends geschlossen hat wie es sollte, weil sich irgendwo ein mieser kleiner Fehler eingeschlichen hat, der so selten war, dass er beim Testen nie aufgetreten ist.
    Da hätte ich jetzt gerne eine Software gehabt, wo ich das Logo-Programm lade, dann eine Bedingung á la "Uhrzeit > 20:00h || Uhrzeit < 06:00h => Tor zu" eingebe (was nun wirklich nicht viel Arbeit ist) und hätte alle Fälle aufgelistet bekommen, in denen dies nicht der Fall ist. Neben einigen legitimen Fällen ware auch der unerwartete dabei gewesen und ich hätte auf die Frage "Geht das Tor jetzt heute abend auch zu?" mit Gewissheit "Ja!" antworten können.

    Bei einer größeren Steuerung stelle ich mir das so vor (korrigiert mich bitte wenn ich falsch liege): Ich muss ich ja auch hier nur das Wichtigste prüfen. Ich kann mir zum Beispiel alle Fälle anzeigen lassen, in denen ein Förderband stillsteht. Oder wenn ich eine Joghurtabfüllmaschine programmiere dann teste ich halt zwischendurch kurz "Wenn Ventil offen dann binnen 30 s Ventil wieder zu". Die Syntax für die Eingabe der Bedingungen muss natürlich intuitiv und simpel sein, ansonsten hat da niemand Lust drauf, ist schon klar.

    Erschwerend kommt hinzu, dass die SPS-Software ja nicht alleine dasteht, es gibt noch die Visualisierung, welche mittlerweile eine sehr großen Umfang besitzt. Also müsste für einen automatisierten Softwaretest auch automatisch Eingaben in der Visu vorgenommen werden... und das ist schon schwieriger ohne die Visu selbst zu manipulieren...
    Das ist natürlich auch richtig, ein automatischer Test des UI ist wohl prinzipiell quasi unmöglich. Allerdings sind die Fehler in der Visualisierung ja weniger tragisch als im Steuerungsablauf. Außerdem: Ein- und Ausgaben in der Visualisierung werden doch als rohe Daten mit der Steuerung kommuniziert und könnten hier, genau wie Ein- und Ausgänge, getestet werden. Wenn man denn unbedingt will.

Ähnliche Themen

  1. Umfrage Gehalt
    Von waldy im Forum Stammtisch
    Antworten: 28
    Letzter Beitrag: 03.01.2012, 15:35
  2. Umfrage Betriebssystem
    Von Ralf62 im Forum HMI
    Antworten: 1
    Letzter Beitrag: 19.09.2010, 22:53
  3. Verifikation und Dokumentation
    Von INST im Forum Maschinensicherheit - Normen und Richtlinien
    Antworten: 2
    Letzter Beitrag: 16.12.2009, 21:55
  4. Umfrage zu Studienarbeit
    Von S7_Student im Forum CODESYS und IEC61131
    Antworten: 19
    Letzter Beitrag: 19.05.2009, 16:27

Lesezeichen

Berechtigungen

  • Neue Themen erstellen: Nein
  • Themen beantworten: Nein
  • Anhänge hochladen: Nein
  • Beiträge bearbeiten: Nein
  •