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:
High Through-Put VLSI Architecture for FFT Computation Kapitel lesen Erstes Kapitel lesen

2013 | OriginalPaper | Buchkapitel

13. Developing Embedded Systems from Formal Specifications Written in Temporal Logic

verfasst von : Shigeki Hagihara, Takahiro Arai, Masaya Shimakawa, Naoki Yonezaki

Erschienen in: Proceedings of the Third International Conference on Trends in Information, Telecommunication and Computing

Verlag: Springer New York

Einloggen

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

search-config
loading …

Abstract

We propose a semi-automatic method for developing embedded systems using program code extraction from formal specifications written in temporal logic. This method consists of the following four steps. (1) Write a formal specification for a system. (2) Refine the specification to adapt to the structure and function of the hardware. (3) Obtain a transition system representing a program from the refined specification. (4) Assign program codes to atomic propositions used in the specification, and convert the transition system to the program. As a case study to demonstrate that the proposed method is practical, we generate a program which controls a robot as a line tracer.

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
Vorheriges Kapitel A Comparative Review of Contention-Aware Scheduling Algorithms to Avoid Contention in Multicore Systems
Nächstes Kapitel Network Log Clustering Using K-Means Algorithm
Literatur
1.
2.
Tomita T, Hagihara S, Yonezaki N (2011) A probabilistic temporal logic with frequency operators and its model checking. In: Proceedings of the 13th international workshop on verification of infinite-state systems. EPTCS, vol 73. pp 79–93
3.
Abadi M, Lamport L, Wolper P (1989) Realizable and unrealizable specifications of reactive systems. In: Proceedings of 16th international colloquium on automata, languages, and programming. LNCS, vol 372. Springer. pp 1–17
4.
Pnueli A, Rosner R (1989) On the synthesis of a reactive module. In: Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on principles of programming languages. pp. 179–190
5.
6.
Vanitha V, Yamashita K, Fukuzawa K, Yonezaki N (2000) A method for structuralisation of evolutional specifications of reactive systems. In: ICSE 2000. The third international workshop on intelligent software engineering. pp 30–38
7.
Hagihara S, Yonezaki N (2006) Completeness of verification methods for approaching to realizable reactive specifications. In: Proceedings of 1st Asian working conference on verified software AWCVS’06. UNU-IIST, vol 348. pp 242—257
8.
Hagihara S, Kitamura Y, Shimakawa M, Yonezaki N (2009) Extracting environmental constraints to make reactive system specifications realizable. In: Proceedings of the 2009 16th Asia-pacific software engineering conference. APSEC ‘09, IEEE Computer Society. pp 61—68
9.
10.
Jobstmann B, Bloem R (2006) Optimizations for LTL synthesis. In: Formal methods in computer aided design, 2006 (FMCAD ‘06). pp 117–124
11.
Koymans R (1990) Specifying real-time properties with metric temporal logic. Real-Time Syst 2(4):255–299CrossRef
12.
13.
Raskin JF, Schobbens PY (1998) The logic of event clocks: decidability, complexity and expressiveness. Automatica 34(3):247–282MathSciNet
14.
Doyen L, Geeraerts G, Raskin JF, Reichert J (2009) Realizability of real-time logics. In: Proceedings of the 7th international conference on formal modeling and analysis of timed systems. FORMATS ‘09, Springer-Verlag. pp 133–148
15.
Maler O, Nickovic D, Pnueli A (2007) On synthesizing controllers from bounded-response properties. In: Proceedings of the 19th international conference on Computer aided verification (CAV’07). Springer-Verlag, pp 95–107
Metadaten
Titel
Developing Embedded Systems from Formal Specifications Written in Temporal Logic
verfasst von
Shigeki Hagihara
Takahiro Arai
Masaya Shimakawa
Naoki Yonezaki
Copyright-Jahr
2013
Verlag
Springer New York
Buch
Proceedings of the Third International Conference on Trends in Information, Telecommunication and Computing

Print ISBN: 978-1-4614-3362-0

Electronic ISBN: 978-1-4614-3363-7

Copyright-Jahr: 2013

DOI
https://doi.org/10.1007/978-1-4614-3363-7_13

Neuer Inhalt

    Bildnachweise