著者
Beuran Razvan Chinen Ken-ichi Tan Yasuo Shinoda Yoichi
出版者
北陸先端科学技術大学院大学先端科学技術研究科情報科学系
雑誌
Research report (School of Information Science, Graduate School of Advanced Science and Technology, Japan Advanced Institute of Science and Technology) (ISSN:09187553)
巻号頁・発行日
vol.IS-RR-2016-003, pp.1-16, 2016-10-14

Effective cybersecurity education and training are important for preparing current and future IT professionals to properly and swiftly deal withreal-life security incidents. In this paper we use the main cybersecurity training programs in Japan as a detailed case study for analyzing the best practices and methodologies in the field of cybersecurity education and training. Based on this analysis and our first-hand experience with some of the said training programs, we then define the requirements that must be met in order to ensure effective cybersecurity education and training.Finally, we discuss our research and development endeavor towards creating a framework that meets these requirements, so as to facilitate effectiveeducation and training in cybersecurity.
著者
Aoki Toshiaki Satoh Makoto Tani Mitsuhiro Yatake Kenro Kishi Tomoji
出版者
北陸先端科学技術大学院大学先端科学技術研究科情報科学系
雑誌
Research report (School of Information Science, Graduate School of Advanced Science and Technology, Japan Advanced Institute of Science and Technology) (ISSN:09187553)
巻号頁・発行日
vol.IS-RR-2016-002, pp.1-11, 2016-05-23

The safety and reliability of automotive systems are becoming a big concern in our daily life. Recently, a functional safety standard which specializes in automotive systems has been proposed by the ISO. In addition, electrical throttle systems have been inspected by NHTSA and NASA due to the unintended acceleration problems of Toyota’s cars. In light of such recent circumstances, we are researching practical applications of formal methods to ensure the high quality of automotive operating systems. An operating system which we focus on is the one conforming to the OSEK/VDX standard. This paper shows a case study where model checking is applied to a commercial automotive operating system. In this case study, the model checking is combined with testing in order to efficiently and effectively verify it. As a result, we acquired the confidence that the quality of the operating system is very high.