This is a special issue of ACM TECS consisting of selected papers of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE 2017). MEMOCODE's general objective is to bring together researchers and practitioners interested in formal methods and models for system design and development to exchange ideas, research results, and lessons learned. System design covers the design and development of hardware, firmware, middleware, and application software for systems ranging from single embedded devices to highly networked CPS and systems in the internet of things (IoT). MEMOCODE emphasizes the importance of formal models and methods in correct system design in all aspects of computer system development. In particular, MEMOCODE focuses on research contributions and formal foundations, engineering methods, tools, and experimental case studies. MEMOCODE 2017 took place in Vienna (Austria) and was co-located with the conference on Formal Methods in Computer-Aided Design (FMCAD) as in some previous years. Among the 48 papers submitted to MEMOCODE 2017, we have selected the following six papers for inclusion in this special issue that show the broad spectrum of MEMOCODE's field of interest which covers all phases of system design:-Modeling: 'Stochastic Assume-Guarantee Contracts for Cyber-Physical System Design' Li presents an assume-guarantee contract framework for the design of cyber-physical systems under probabilistic requirements. System behaviors, assumptions, and guarantees are described by a stochastic signal temporal logic. For certain systems, the approach can check contract compatibility, consistency, and refinement, and can generate a controller to guarantee that a contract is satisfied.-Verification: 'Mining Missing Assumptions from Counter-Examples' by Guillaume Plassan, Katell Morin-Allory, and Dominique Borrione observed that in formal verification of register-transfer level hardware designs, one often experiences false failures due to under-constrained models. The approach extracts the missing assumptions from counterexamples to help the designers to correct their models.-Testing: 'Model-based, mutation-driven test case generation via heuristic-guided branching' by Andreas Fellner, Willibald Krenn, Thorsten Tarrach, Georg Weis-senbacher, and Rupert Schlick introduces an algorithmic framework for parallel heuristic-guided searches for test case generation of action systems. Since no single heuristic is able to find all the mutants that are found by the others, the best result is achieved by running multiple heuristics independently and combining their results.-Synthesis: 'Compositional Dataflow Circuits' by Stephen A. Edwards, Richard Townsend, and Martha A. Kim presents a technique for implementing dataflow networks as compositional hardware circuits. Based on a first abstract dataflow model with unbounded buffers that supports data-dependent blocks (mux, demux, and non-deterministic merge), it is shown how to faithfully implement such networks with bounded buffers and handshaking in a compositional synthesis procedure. Insert