Applying Multi-Core Model Checking to Hardware-Software Partitioning in Embedded Systems (extended version)
作者： Lucas C. Cordeiro , Hussama Ismail , Alessandro Trindade
DOI:
关键词:
摘要: We present an alternative approach to solve the hardware (HW) and software (SW) partitioning problem, which uses Bounded Model Checking (BMC) based on Satisfiability Modulo Theories (SMT) in conjunction with a multi-core support using Open Multi-Processing. The SMT-based BMC allows initializing many verification instances processors cores numbers available model checker. Each instance checks for different optimum value until optimization problem is satisfied. goal show that model-checking techniques can be effective, particular cases, find optimal solution of HW-SW approach. compare experimental results our proposed Integer Linear Programming Genetic Algorithm.
arxiv.org
harvard.edu参考文章(29)
Nikolaj Bjørner, Anh-Dung Phan, Lars Fleckenstein, νZ - An Optimizing SMT Solver Tools and Algorithms for the Construction and Analysis of Systems. pp. 194- 199 ,(2015) , 10.1007/978-3-662-46681-0_14
Leonardo de Moura, Nikolaj Bjørner, Z3: an efficient SMT solver tools and algorithms for construction and analysis of systems. pp. 337- 340 ,(2008) , 10.1007/978-3-540-78800-3_24
Gerard J. Holzmann, Parallelizing the spin model checker international workshop on model checking software. pp. 155- 171 ,(2012) , 10.1007/978-3-642-31759-0_12
Joost-Pieter Katoen, Christel Baier, Principles of Model Checking ,(2008)
Singiresu S. Rao, Engineering Optimization : Theory and Practice ,(2011)
Robert Brummayer, Armin Biere, Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays tools and algorithms for construction and analysis of systems. pp. 174- 177 ,(2009) , 10.1007/978-3-642-00768-2_16
Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Ofer Strichman, Yunshan Zhu, Bounded Model Checking Advances in Computers. ,vol. 58, pp. 117- 148 ,(2003) , 10.1016/S0065-2458(03)58003-2
Christoph M. Wintersteiger, Youssef Hamadi, Leonardo de Moura, A Concurrent Portfolio Approach to SMT Solving Computer Aided Verification. pp. 715- 720 ,(2009) , 10.1007/978-3-642-02658-4_60
M.R. Guthaus, T. Mudge, R.B. Brown, D. Ernst, T.M. Austin, J.S. Ringenberg, MiBench: A free, commercially representative embedded benchmark suite ieee international symposium on workload characterization. pp. 3- 14 ,(2001) , 10.1109/WWC.2001.15
Luhe Hong, Jianli Cai, The application guide of mixed programming between MATLAB and other programming languages international conference on computer and automation engineering. ,vol. 3, pp. 185- 189 ,(2010) , 10.1109/ICCAE.2010.5452058