Specification and Automated Verification of Dynamic Dataflow Networks

  • Jonatan WiikEmail author
  • Pontus Boström
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10469)


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.


  1. 1.
    Ahrendt, W., Dylla, M.: A system for compositional verification of asynchronous objects. Sci. Comput. Program. 77(12), 1289–1309 (2012)CrossRefGoogle Scholar
  2. 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_17CrossRefGoogle Scholar
  3. 3.
    Boström, P., Wiik, J.: Contract-based verification of discrete-time multi-rate Simulink models. Softw. Syst. Modeling 15(4), 1141–1161 (2016)CrossRefGoogle Scholar
  4. 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)MathSciNetCrossRefGoogle Scholar
  5. 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_24CrossRefGoogle Scholar
  6. 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_24CrossRefGoogle Scholar
  7. 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. 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_14CrossRefGoogle Scholar
  9. 9.
    Kahn, G.: The semantics of a simple language for parallel programming. In: Information Processing 1974 (1974)Google Scholar
  10. 10.
    Lee, E.A., Messerschmitt, D.G.: Synchronous data flow. Proc. IEEE 75(9), 1235–1245 (1987)CrossRefGoogle Scholar
  11. 11.
    Lee, E.A., Parks, T.M.: Dataflow process networks. Proc. IEEE 83(5), 773–799 (1995)CrossRefGoogle Scholar
  12. 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)CrossRefGoogle Scholar
  13. 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_27CrossRefGoogle Scholar
  14. 14.
    Mattavelli, M., Amer, I., Raulet, M.: The reconfigurable video coding standard. IEEE Signal Process. Mag. 27(3), 159–167 (2010)CrossRefGoogle Scholar
  15. 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. 16.
    Wiik, J., Boström, P.: Specification and automated verification of dynamic dataflow networks. Technical report 1170, TUCS (2016)Google Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.Faculty of Science and EngineeringÅbo Akademi UniversityTurkuFinland

Personalised recommendations