Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Termination Analysis of Probabilistic Programs Through Positivstellensatz’s Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Structural Synthesis for GXW Specifications

verfasst von : Chih-Hong Cheng, Yassine Hamza, Harald Ruess

Erschienen in: Computer Aided Verification

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

We define the \(\textsf {\small {GXW}} \) fragment of linear temporal logic (LTL) as the basis for synthesizing embedded control software for safety-critical applications. Since \(\textsf {\small {GXW}} \) includes the use of a weak-until operator we are able to specify a number of diverse programmable logic control (PLC) problems, which we have compiled from industrial training sets. For \(\textsf {\small {GXW}} \) controller specifications, we develop a novel approach for synthesizing a set of synchronously communicating actor-based controllers. This synthesis algorithm proceeds by means of recursing over the structure of \(\textsf {\small {GXW}} \) specifications, and generates a set of dedicated and synchronously communicating sub-controllers according to the formula structure. In a subsequent step, 2QBF constraint solving identifies and tries to resolve potential conflicts between individual \(\textsf {\small {GXW}} \) specifications. This structural approach to \(\textsf {\small {GXW}} \) synthesis supports traceability between requirements and the generated control code as mandated by certification regimes for safety-critical software. Our experimental results suggest that GXW synthesis scales well to industrial-sized control synthesis problems with 20 input and output ports and beyond.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel PSCV: A Runtime Verification Tool for Probabilistic SystemC Models
Nächstes Kapitel Bounded Cycle Synthesis
Fußnoten
1
The formal operational semantics, as it is standardized notation from SDF, is relegated to [1].
 
3
For pattern type P2 or P3, one needs to have each clause formula of \(\phi ^{i}_{in}\) be of form \(\chi ^i_{in}\), i.e., the highest number of consecutive X should equal i. The purpose is to align \(\chi ^i_{in}\) with the preceding \(\mathbf X ^{i}\) in \(\mathbf G (\phi ^i_{in} \rightarrow \mathbf X ^i (\varrho _{out}\,\mathbf W \, (\varphi ^{j}_{in} \vee \rho ^0_{out})) )\) or \(\mathbf G (\phi ^i_{in} \rightarrow \mathbf X ^i \varrho _{out})\). If a clause formula in DNF contains no literal starting with \(\mathbf X ^i\), one can always pad a conjunction \(\mathbf X ^i\,\textsf {\small {{true}}}\) to the clause formula. The padding is not needed for P1.
 
4
Quantified Boolean Formula with one top-level quantifier alternation.
 
5
Even without unroll, one can infer relations over universal variables via statically analyzing the specification. As an example, consider two sub-specifications \(S1: \mathbf G (\textsf {\small {{in1}}} \rightarrow (\textsf {\small {{out}}}\,\mathbf W \,\textsf {in2}))\) and \(S2: \mathbf G (\textsf {\small {{in2}}} \rightarrow (\lnot \textsf {\small {{out}}} \,\mathbf W \, \textsf {\small {{in1}}}))\). One can infer that it is impossible for \(TrUB^{(1)}\) and \(TrUB^{(2)}\) to be simultaneously have state variable \(lock=\textsf {\small {{true}}}\), as both starts with \(lock=\textsf {\small {{false}}}\), and if S1 first enters lock \((lock=\textsf {\small {{true}}})\) due to \(\textsf {\small {{in1}}}\), the S2 cannot enter, as release part of S2 is also \(\textsf {\small {{in1}}}\). Similar argument follows vice versa.
 
6
Rejecting feedback loops on the controller structure is only a restriction of our presented method and is not the reason for unrealizability; similar to Fig. 7, feedback loop can possibly be resolved by merging all actors involving feedback to a single actor.
 
7
A counter-strategy in LTL synthesis a state machine where the environment can enforce to violate the given property, regardless of all possible moves by the controller [27].
 
8
Approximately 0.25 seconds is used for initializing JVM in every run.
 
Literatur
1.
2.
3.
4.
5.
Bloem, R., Cimatti, A., Greimel, K., Hofferek, G., Könighofer, R., Roveri, M., Schuppan, V., Seeber, R.: RATSY – a new requirements analysis tool with synthesis. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 425–429. Springer, Heidelberg (2010)CrossRef
6.
Bloem, R., Ehlers, R., Jacobs, S., Knighofer, R.: How to handle assumptions in synthesis. In: SYNT, pp. 34–50 (2014). EPTCS 157
7.
Bloem, R., Könighofer, B., Könighofer, R., Wang, C.: Shield synthesis: runtime enforcement for reactive systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 533–548. Springer, Heidelberg (2015)
8.
Bohy, A., Bruyère, V., Filiot, E., Jin, N., Raskin, J.-F.: Acacia+, a tool for LTL synthesis. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 652–657. Springer, Heidelberg (2012)CrossRef
9.
Brenguier, R., Prez, G.A., Raskin, J.-F., Sankur, O.: AbsSynthe: abstract synthesis from succinct safety specifications. In: SYNT, pp. 100–116 (2014). EPTCS 157
10.
Cheng, C.-H., Huang, C.-H., Ruess, H., Stattelmann, S.: \({{\sf G4LTL-ST}}\): automatic generation of PLC programs. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 541–549. Springer, Heidelberg (2014)
11.
Ehlers, R.: Unbeast: symbolic bounded synthesis. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 272–275. Springer, Heidelberg (2011)CrossRef
12.
Eker, J., Janneck, J., Lee, E.A., Liu, J., Liu, X., Ludvig, J., Sachs, S., Xiong, Y.: Taming heterogeneity - the Ptolemy approach. Proc. IEEE 91(1), 127–144 (2003)CrossRef
13.
Jacobs, S., Bloem, R., Brenguier, R., Ehlers, R., Hell, T., Knighofer, R. Prez, G.A., Raskin, J.-F., Ryzhyk, L., Sankur, O., Seidl, M., Tentrup, L., Walker, A.: The first reactive synthesis competition. In: SYNTCOMP 2014 (2014). http://​arxiv.​org/​abs/​1506.​08726
14.
Jobstmann, B., Bloem, R.: Optimizations for LTL synthesis. In: FMCAD, pp. 117–124. IEEE (2006)
15.
Jobstmann, B., Galler, S., Weiglhofer, M., Bloem, R.: Anzu: a tool for property synthesis. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 258–262. Springer, Heidelberg (2007)CrossRef
16.
17.
18.
Lee, E.A., Messerschmitt, D.G.: Static scheduling of synchronous data flow programs for digital signal processing. IEEE Trans. Comput. 36(1), 24–35 (1987)CrossRef
19.
Lee, E.A., Messerschmitt, D.G.: Synchronous data flow. Proc. IEEE 75(9), 1235–1245 (1987)CrossRef
20.
Li, W.-C.: Specification mining: new formalisms, algorithms and applications. Ph.D. thesis. UC Berkeley (2015)
21.
Lonsing, F., Biere, A.: DepQBF: a dependency-aware QBF solver. J. Satisfiability Boolean Model. Comput. 7, 71–76 (2010)
22.
Lustig, Y., Vardi, M.Y.: Synthesis from component libraries. STTT 15(5–6), 603–618 (2013)CrossRefMATH
23.
Mavin, A., Wilkinson, P., Harwood, A., Novak, M.: Easy Approach to Requirements Syntax (EARS). In: RE, pp. 317–322. IEEE (2009)
24.
Petry, J.: IEC 61131–3 mit CoDeSys V3: Ein Praxisbuch fuer SPS-Programmierer. Eigenverlag 3S-Smart Software Solutions. ISBN 978-3-000465-08-6 (2011)
25.
Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of reactive(1) designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 364–380. Springer, Heidelberg (2006)CrossRef
26.
Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46–57. IEEE (1977)
27.
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179–190. IEEE (1989)
28.
Schewe, S., Finkbeiner, B.: Bounded synthesis. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 474–488. Springer, Heidelberg (2007)CrossRef
29.
30.
31.
Wong, K.-W., Ehlers, R., Kress-Gazit, H.: Correct high-level robot behavior in environments with unexpected events. In: Robotics: Science and Systems X (RSS X) (2014)
Metadaten
Titel
Structural Synthesis for GXW Specifications
verfasst von
Chih-Hong Cheng
Yassine Hamza
Harald Ruess
Copyright-Jahr
2016
Buch
Computer Aided Verification

Print ISBN: 978-3-319-41527-7

Electronic ISBN: 978-3-319-41528-4

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-41528-4_6

Premium Partner

    Bildnachweise