Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Formal Methods for Industrial Critical Systems

FMICS 2012: Formal Methods for Industrial Critical Systems pp 63–77Cite as

Microcontroller Assembly Synthesis from Timed Automaton Task Specifications

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 7437))

Abstract

A method for the automatic refinement of single-task timed automaton specifications into microcontroller assembly code is proposed. The outputs of the refinement are an assembly implementation and a timed automaton describing its exact behaviour. Implementation is only possible when all specified timing behaviours can be met by the target microcontroller. Crucially, the implementation does not make the simplifying synchrony assumption, yet correctness with respect to timing is guaranteed. Currently this method copes with parallel inputs and outputs, but is restricted to timed automaton specifications with only one clock variable that is reset after each transition. Further generalization is possible. A tool illustrates the method on a simple example.

This research is supported by the National Science and Engineering Research Council of Canada (NSERC).

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   49.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  2. Amnell, T., Fersman, E., Mokrushin, L., Pettersson, P., Yi, W.: TIMES: A Tool for Schedulability Analysis and Code Generation of Real-time Systems. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 60–72. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  3. Bandur, V.: Hard Real-Time Microcontroller Code Generation from Timed Automaton Specifications. Master’s thesis, McMaster University (2008), http://www.cs.york.ac.uk/~bandurvp

  4. Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: UPPAAL-Tiga: Time for Playing Games! In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 121–125. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  5. De Wulf, M., Doyen, L., Raskin, J.F.: Almost ASAP semantics: From timed models to timed implementations. Formal Aspects of Computing 17(3), 319–341 (2005)

    Article  MATH  Google Scholar 

  6. Dierks, H.: PLC-automata: A New Class of Implementable Real-time Automata. In: Bertrán, M., Rus, T. (eds.) ARTS 1997. LNCS, vol. 1231, pp. 111–125. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  7. Dierks, H.: Synthesizing controllers from real-time specifications. IEEE Trans. on CAD of Integrated Circuits and Systems 18(1), 33–43 (1999)

    Article  Google Scholar 

  8. Dierks, H.: PLC-automata: A new class of implementable real-time automata. Theoretical Computer Science 253 (2001)

    Google Scholar 

  9. Freescale Semiconductor: MC68HC08AB16A/D Data Sheet (July 2005), document MCH68HC08AB16A

    Google Scholar 

  10. Graphviz: Graphviz – graph visualization software (2011), http://www.graphviz.org

  11. Intel Corporation: Intel MCS 51 Microcontroller Family User’s Manual (February 1994), order 272383-002

    Google Scholar 

  12. Jee, E., Wang, S., Kim, J.-K., Lee, J., Sokolsky, O., Lee, I.: A safety-assured development approach for real-time software. In: RTCSA 2010, pp. 133–142. IEEE Computer Society (2010)

    Google Scholar 

  13. Jessen, J.J., Rasmussen, J.I., Larsen, K.G., David, A.: Guided Controller Synthesis for Climate Controller Using Uppaal Tiga. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 227–240. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  14. McEwan, A.A., Woodcock, J.: Unifying Theories of Interrupts. In: Butterfield, A. (ed.) UTP 2008. LNCS, vol. 5713, pp. 122–141. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  15. McKeeman, W.M.: Peephole optimization. Commun. ACM 8(7), 443–444 (1965)

    Article  Google Scholar 

  16. Microchip Technology Inc.: PIC 18FXX2 Data Sheet (2002), document DS39564B

    Google Scholar 

  17. Mukund, M.: Finite-state automata on infinite inputs. Tech. Rep. TCS-96-2, SPIC Mathematical Institute (1996)

    Google Scholar 

  18. Tektronix, Inc.: TDS1000- and TDS2000-Series Digital Storage Oscilloscope (May 2011), document 071-1064-00

    Google Scholar 

  19. Tuttle, M.R., Lynch, N.A.: An introduction to input/output automata. CWI Quarterly 2(3), 219–246 (1989)

    MathSciNet  MATH  Google Scholar 

  20. Wassyng, A., Lawford, M., Hu, X.: Timing Tolerances in Safety-Critical Software. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 157–172. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  21. ChaoChen, Z., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Information Processing Letters 40(5), 269–276 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  22. Zilog: Zilog Z80 Family CPU User Manual (2004), document UM008005-0205

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. The University of York, York, UK

    Victor Bandur

  2. McMaster University, Hamilton, Canada

    Wolfram Kahl & Alan Wassyng

Authors
  1. Victor Bandur
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Wolfram Kahl
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alan Wassyng
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Formal Methods and Tools, University of Twente, P.O. Box 217, 7500 AE, Enschede, The Netherlands

    Mariëlle Stoelinga

  2. Infrastructure and Cities Sector, Mobility and Logistics Division, Rail Automation, Siemens AG, Ackerstraße 22, 38126, Braunschweig, Germany

    Ralf Pinger

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bandur, V., Kahl, W., Wassyng, A. (2012). Microcontroller Assembly Synthesis from Timed Automaton Task Specifications. In: Stoelinga, M., Pinger, R. (eds) Formal Methods for Industrial Critical Systems. FMICS 2012. Lecture Notes in Computer Science, vol 7437. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32469-7_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-32469-7_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-32468-0

  • Online ISBN: 978-3-642-32469-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation