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:
Formal Models and Analysis for Self-adaptive Cyber-physical Systems Kapitel lesen Erstes Kapitel lesen

2017 | OriginalPaper | Buchkapitel

Constrained Synthesis from Component Libraries

verfasst von : Antonio Iannopollo, Stavros Tripakis, Alberto Sangiovanni-Vincentelli

Erschienen in: Formal Aspects of Component Software

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

Synthesis from component libraries is the problem of building a network of components from a given library, such that the network realizes a given specification. This problem is undecidable in general. It becomes decidable if we impose a bound on the number of chosen components. However, the bounded problem remains computationally hard and brute-force approaches do not scale. In this paper we study scalable methods for solving the problem of bounded synthesis from libraries, proposing a solution based on the CounterExample-Guided Inductive Synthesis paradigm. Although our synthesis algorithm does not assume a specific formalism a priori, we present a parallel implementation which instantiates components defined as Linear Temporal Logic-based Assume/Guarantee Contracts. We show the potential of our approach and evaluate our implementation by applying it to an industrial case study.

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 Checking Multi-view Consistency of Discrete Systems with Respect to Periodic Sampling Abstractions
Nächstes Kapitel MARTE/pCCSL: Modeling and Refining Stochastic Behaviors of CPSs with Probabilistic Logical Clocks
Fußnoten
1
Without loss of generality, here we can consider the poset T being organized as a tree. This is enough to obtain a simple type system with single inheritance, where all the types share the same root type (\(\bot \)).
 
2
To indicate \(\rho (p,q)=1\), we will often use the shorthand \(\rho _{p,q}\), and \(\lnot \rho _{p,q}\) for \(\rho (p,q)=0\).
 
3
Just recall that the maximum number of edges in a graph of n nodes is \(\frac{n(n-1)}{2}\). \(2^{\frac{n(n-1)}{2}}\) enumerates all the subsets of those connections.
 
4
Here we borrow the notation typical of first order logic formulas, although all the formulas refer to a finite number of elements.
 
5
This means that, given two components \(G_1\) and \(G_2\), if \(G_1\) has more legal inputs and less legal outputs than \(G_2\) then \(G_1\) can be used in place of \(G_2\).
 
6
Single line diagrams are usually used to simplify the description of three-phase power systems.
 
Literatur
1.
Semiconductor IP Market by Form Factor (ICs IP, SOCs IP), Design Architecture (IP cores (Hard IP, Soft IP), Standard IP, Custom IP, Processor Design), Processor Type (Microprocessor, DSP), Verification IP - Global forecast to 2022. marketsandmarkets.com (2016)
2.
de Alfaro, L., Henzinger, T.A.: Interface automata. In: Proceedings of the 8th European Software Engineering Conference Held Jointly with 9th ACM SIGSOFT International Symposium on Foundations of Software Engineering, ESEC/FSE-9, pp. 109–120. ACM, New York (2001)
3.
Alur, R., Moarref, S., Topcu, U.: Compositional synthesis with parametric reactive controllers. In: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, HSCC 2016, pp. 215–224. ACM, New York (2016)
4.
Benveniste, A., Caillaud, B., Ferrari, A., Mangeruca, L., Passerone, R., Sofronis, C.: Multiple viewpoint contract-based specification and design. In: Boer, F.S., Bonsangue, M.M., Graf, S., Roever, W.-P. (eds.) FMCO 2007. LNCS, vol. 5382, pp. 200–225. Springer, Heidelberg (2008). doi:10.​1007/​978-3-540-92188-2_​9 CrossRef
5.
Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334–342. Springer, Cham (2014). doi:10.​1007/​978-3-319-08867-9_​22
6.
Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000). doi:10.​1007/​10722167_​15 CrossRef
7.
8.
Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthesis of loop-free programs. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, pp. 62–73. ACM, New York (2011)
9.
Iannopollo, A., Nuzzo, P., Tripakis, S., Sangiovanni-Vincentelli, A.: Library-based scalable refinement checking for contract-based design. In: Design, Automation and Test in Europe Conference and Exhibition (DATE), pp. 1–6, March 2014
10.
Jha, S., Seshia, S.A.: A theory of formal synthesis via inductive learning. CoRR abs/1505.03953 (2015)
11.
12.
Moir, I., Seabridge, A.: Aircraft Systems: Mechanical, Electrical and Avionics Subsystems Integration, 3rd edn. Wiley, Chichester (2008)CrossRef
13.
Nuzzo, P., Finn, J., Iannopollo, A., Sangiovanni-Vincentelli, A.: Contract-based design of control protocols for safety-critical cyber-physical systems. In: Design, Automation and Test in Europe Conference and Exhibition (DATE), pp. 1–4, March 2014
14.
Nuzzo, P., Iannopollo, A., Tripakis, S., Sangiovanni-Vincentelli, A.: Are interface theories equivalent to contract theories? In: 2014 Twelfth ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), pp. 104–113, October 2014
15.
Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: 31st Annual Symposium on Foundations of Computer Science, Proceedings, vol. 2, pp. 746–757, October 1990
16.
Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science, SFCS 1977, pp. 46–57. IEEE Computer Society, Washington, DC (1977)
17.
Sangiovanni-Vincentelli, A.: Quo vadis, SLD? Reasoning about the trends and challenges of system level design. Proc. IEEE 95(3), 467–506 (2007)CrossRef
18.
Sangiovanni-Vincentelli, A., Damm, W., Passerone, R.: Taming Dr. Frankenstein: contract-based design for cyber-physical systems. Eur. J. Control 18(3), 217–238 (2012)MathSciNetCrossRefMATH
19.
Seshia, S.A.: Combining induction, deduction, and structure for verification and synthesis. Proc. IEEE 103(11), 2036–2051 (2015)CrossRef
20.
Shapiro, E.Y.: Algorithmic Program DeBugging. MIT Press, Cambridge (1983)MATH
21.
22.
Solar-Lezama, A., Tancau, L., Bodik, R., Seshia, S., Saraswat, V.: Combinatorial sketching for finite programs. SIGOPS Oper. Syst. Rev. 40(5), 404–415 (2006)CrossRef
23.
Wongpiromsarn, T., Topcu, U., Ozay, N., Xu, H., Murray, R.M.: Tulip: a software toolbox for receding horizon temporal logic planning. In: Proceedings of the 14th International Conference on Hybrid Systems: Computation and Control, HSCC 2011, pp. 313–314. ACM, New York (2011)
Metadaten
Titel
Constrained Synthesis from Component Libraries
verfasst von
Antonio Iannopollo
Stavros Tripakis
Alberto Sangiovanni-Vincentelli
Copyright-Jahr
2017
Buch
Formal Aspects of Component Software

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

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

Copyright-Jahr: 2017

DOI
https://doi.org/10.1007/978-3-319-57666-4_7