Research ArticleOpen AccessGoogle Scholar indexed
Specification and Verification of Dynamically Reconfigurable Systems Using Dynamic Linear Hybrid Automata
Graduate School of Natural Science & Technology, Kanazawa University, Kanazawa, Japan
Graduate School of Natural Science & Technology, Kanazawa University, Kanazawa, Japan
Graduate School of Natural Science & Technology, Kanazawa University, Kanazawa, Japan
Institute of Science and Engineering, Kanazawa University, Kanazawa, Japan
- 1 Graduate School of Natural Science & Technology, Kanazawa University, Kanazawa, Japan
- 2 Graduate School of Natural Science & Technology, Kanazawa University, Kanazawa, Japan
- 3 Graduate School of Natural Science & Technology, Kanazawa University, Kanazawa, Japan
- 4 Institute of Science and Engineering, Kanazawa University, Kanazawa, Japan
Journal of Software Engineering and Applications·Volume 09 (2016)·Pages 452–478·Published 7 September 2016·DOI10.4236/jsea.2016.99030
Copy link · social · email
Abstract
A dynamically reconfigurable system can change its configuration during operation, and studies of such systems are being carried out in many fields. In particular, medical technology and aerospace engineering must ensure system safety because any defect will have serious consequences. Model checking is a method for verifying system safety. In this paper, we propose the Dynamic Linear Hybrid Automaton (DLHA) specification language and show a method to analyze reachability for a system consisting of several DLHAs.
KeywordsFormal MethodModel CheckingHybrid AutomataEmbedded SystemsDynamically Reconfigurable Systems
- Agirre, A., Parra, J., Armentia, A., Estévez, E. and Marcos, M. (2016) QoS Aware Middleware Support for Dynamically Reconfigurable Component Based IoT Applications. International Journal of Distributed Sensor Networks, 2016, Article ID: 2702789. http://dx.doi.org/10.1155/2016/2702789
- Garcia, P., Compton, K., Schulte, M., Blem, E. and Fu, W. (2006) An Overview of Reconfigurable Hardware in Embedded Systems. EURASIP Journal on Embedded Systems, 2006 Article ID: 056320. http://dx.doi.org/10.1186/1687-3963-2006-056320
- Lockwood, J.W., Moscola, J., Kulig, M., Reddick, D. and Brooks, T. (2003) Internet Worm and Virus Protection in Dynamically Reconfigurable Hardware. International Conferences on Military and Aerospace Programmable Logic Device (MAPLD), Washington DC, 9-11 September 2003, E10.
- Motomura, M., Fujii, T., Furuta, K., Anjo, K., Yabe, Y., Togawa, K., Yamada, J., Izawa, Y. and Sasaki, R. (2005) New Generation Microprocessor Architecture (2) Dynamically Reconfigurable Processor (DRP). IPSJ Magazine, 46, 1259-1265.
- Amano, H., Adachi, Y., Tsutsumi, S., Ishikawa, K., et al. (2006) A Context Dependent Clock Control Mechanism for Dynamically Reconfigurable Processors. International Conference on Field Programmable Logic and Applications, 104, 575-580. http://dx.doi.org/10.1109/fpl.2006.311269
- Vatankhahghadim, A., Song, W. and Sheikholeslami, A. (2015) A Variation-Tolerant MRAM-Backed-SRAM Cell for a Nonvolatile Dynamically Reconfigurable FPGA. IEEE Transactions on Circuits and Systems II: Express Briefs, 62, 573-577. http://dx.doi.org/10.1109/TCSII.2015.2407711
- Alur, R., Courcoubetis, C., Henzinger, T.A. and Ho, P. (1993) Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems. Lecture Notes in Computer Science, 736, 209-229. http://dx.doi.org/10.1007/3-540-57318-6_30
- Varshavsky, V. and Marakhovsky, V. (2002) GALA (Globally Asynchronous-Locally Arbitrary) Design. Lecture Notes in Computer Science, 2549, 61-107. http://dx.doi.org/10.1007/3-540-36190-1_3
- Minami, S., Takinai, S., Sekoguchi, S., Nakai, Y. and Yamane, S. (2011) Modeling, Specification and Model Checking of Dynamically Reconfigurable Processors. Computer Software, 28, 190-216.
- Attie, P.C. and Lynch, N.A. (2001) Dynamic Input/Output Automata, a Formal Model for Dynamic Systems. Proceedings of the 20th Annual ACM Symposium on Principles of Distributed Computing (PODC), 2154, 314-316. http://dx.doi.org/10.1145/383962.384051