Skip to main content
SpringerLink
Log in

Specification and Automated Verification of Dynamic Dataflow Networks

  • Conference paper
  • First Online:
Software Engineering and Formal Methods (SEFM 2017)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10469))

Included in the following conference series:

Abstract

Dataflow programming has received much recent attention within the signal processing domain as an efficient paradigm for exploiting parallelism. In dataflow programming, systems are modelled as a static network of actors connected through asynchronous order-preserving channels. In this paper we present an approach to contract-based specification and automated verification of dynamic dataflow networks. The verification technique is based on encoding the dataflow networks and contracts in the guarded command language Boogie.

The work has been partially funded by the Academy of Finland through the projects Merge (No. 286094) and ADVICeS (No. 266373).

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

Access this chapter

Log in via an institution

Institutional subscriptions

Notes

  1. 1.

    http://users.abo.fi/jonwiik/actortool/.

  2. 2.

    http://orcc.sourceforge.net/.

References

  1. Ahrendt, W., Dylla, M.: A system for compositional verification of asynchronous objects. Sci. Comput. Program. 77(12), 1289–1309 (2012)

    Article  Google Scholar 

  2. Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: Boer, F.S., Bonsangue, M.M., Graf, S., Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006). doi:10.1007/11804192_17

    Chapter  Google Scholar 

  3. Boström, P., Wiik, J.: Contract-based verification of discrete-time multi-rate Simulink models. Softw. Syst. Modeling 15(4), 1141–1161 (2016)

    Article  Google Scholar 

  4. Boutellier, J., Ersfolk, J., Lilius, J., Mattavelli, M., Roquier, G., Silvén, O.: Actor merging for dataflow process networks. IEEE Trans. Signal Process. 63(10), 2496–2508 (2015)

    Article  MathSciNet  Google Scholar 

  5. Champion, A., Gurfinkel, A., Kahsai, T., Tinelli, C.: CoCoSpec: a mode-aware contract language for reactive systems. In: De Nicola, R., Kühn, E. (eds.) SEFM 2016. LNCS, vol. 9763, pp. 347–366. Springer, Cham (2016). doi:10.1007/978-3-319-41591-8_24

    Chapter  Google Scholar 

  6. de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  7. Eker, J., Janneck, J.W.: CAL language report. Technical report. ERL Technical Memo UCB/ERL M03/48, University of California at Berkeley (2003)

    Google Scholar 

  8. Jin, Y., Esser, R., Lakos, C., Janneck, J.W.: Modular analysis of dataflow process networks. In: Pezzè, M. (ed.) FASE 2003. LNCS, vol. 2621, pp. 184–199. Springer, Heidelberg (2003). doi:10.1007/3-540-36578-8_14

    Chapter  Google Scholar 

  9. Kahn, G.: The semantics of a simple language for parallel programming. In: Information Processing 1974 (1974)

    Google Scholar 

  10. Lee, E.A., Messerschmitt, D.G.: Synchronous data flow. Proc. IEEE 75(9), 1235–1245 (1987)

    Article  Google Scholar 

  11. Lee, E.A., Parks, T.M.: Dataflow process networks. Proc. IEEE 83(5), 773–799 (1995)

    Article  Google Scholar 

  12. Lee, E.A., Messerschmitt, D.G.: Static scheduling of synchronous data flow programs for digital signal processing. IEEE Trans. Comput. 100(1), 24–35 (1987)

    Article  Google Scholar 

  13. Leino, K.R.M., Müller, P.: A basis for verifying multi-threaded programs. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 378–393. Springer, Heidelberg (2009). doi:10.1007/978-3-642-00590-9_27

    Chapter  Google Scholar 

  14. Mattavelli, M., Amer, I., Raulet, M.: The reconfigurable video coding standard. IEEE Signal Process. Mag. 27(3), 159–167 (2010)

    Article  Google Scholar 

  15. Wandeler, E., Janneck, J.W., Lee, E.A., Thiele, L.: Counting interface automata and their application in static analysis of actor models. In: SEFM 2005. IEEE (2005)

    Google Scholar 

  16. Wiik, J., Boström, P.: Specification and automated verification of dynamic dataflow networks. Technical report 1170, TUCS (2016)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Faculty of Science and Engineering, Åbo Akademi University, Turku, Finland

    Jonatan Wiik & Pontus Boström

Authors
  1. Jonatan Wiik
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Pontus Boström
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jonatan Wiik .

Editor information

Editors and Affiliations

  1. University of Trento, Trento, Italy

    Alessandro Cimatti

  2. Mälardalen University, Västerås, Sweden

    Marjan Sirjani

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Wiik, J., Boström, P. (2017). Specification and Automated Verification of Dynamic Dataflow Networks. In: Cimatti, A., Sirjani, M. (eds) Software Engineering and Formal Methods. SEFM 2017. Lecture Notes in Computer Science(), vol 10469. Springer, Cham. https://doi.org/10.1007/978-3-319-66197-1_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-66197-1_9

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-66196-4

  • Online ISBN: 978-3-319-66197-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation