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.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
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.
References
Ahrendt, W., Dylla, M.: A system for compositional verification of asynchronous objects. Sci. Comput. Program. 77(12), 1289–1309 (2012)
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
Boström, P., Wiik, J.: Contract-based verification of discrete-time multi-rate Simulink models. Softw. Syst. Modeling 15(4), 1141–1161 (2016)
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)
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
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
Eker, J., Janneck, J.W.: CAL language report. Technical report. ERL Technical Memo UCB/ERL M03/48, University of California at Berkeley (2003)
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
Kahn, G.: The semantics of a simple language for parallel programming. In: Information Processing 1974 (1974)
Lee, E.A., Messerschmitt, D.G.: Synchronous data flow. Proc. IEEE 75(9), 1235–1245 (1987)
Lee, E.A., Parks, T.M.: Dataflow process networks. Proc. IEEE 83(5), 773–799 (1995)
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)
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
Mattavelli, M., Amer, I., Raulet, M.: The reconfigurable video coding standard. IEEE Signal Process. Mag. 27(3), 159–167 (2010)
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)
Wiik, J., Boström, P.: Specification and automated verification of dynamic dataflow networks. Technical report 1170, TUCS (2016)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights 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)