Safety verification method for priority-based real-time softwareFumio Narisawa; Yoshikazu Ueda, The number of functions and the sizes of electronic controls and software systems in automobiles are increasing, as ADAS 1 and autonomous driving systems are realized. A higher safety level is also being demanded for complex control systems, so functional safety standards, such as ISO 26262, are increasingly being introduced to in-vehicle systems. In safety-critical systems, failures are diagnosed by the cooperative function of hardware and software. Furthermore, the diagnostic software consists of a mixture of a cyclic execution portion and a hardware-event-driven portion. Testing the cooperative function of multiple concurrent processes is impractically time consuming because the combinations of conditions are so numerous. Formal verification technology is effective because it enables exhaustive verification of a vast quantity of test cases including unexpected states, but a modeling methodology for timing-related uncertainty between hardware events and cyclic software executions has not been established. Our proposed method is to model a combination of the concurrent executions of multiple tasks under non-deterministic event from hardware. We chose the C-language-based model checker CBMC as a verification engine and made an extension to CSeq as a concurrency pre-processor. We proposed the common verification architecture for functional safety software and developed priority-based scheduling mechanism and the event-injection mechanism on CSeq., IOS Press
Frontiers in Artificial Intelligence and Applications, 2017,
[] 組込みシステム検査のための協調解析
Satoru Furukawa; Yoshikazu Ueda; Shin Nakajima
日本ソフトウェア科学会コンピュータソフトウェア, Aug. 2014, []
Realistic Validation of Specification for Modeling Language using AlloyKei Kogai; Yoshikazu Ueda, Authors suggest a resolution to validate metamodels using a formal description language and analyzer Alloy. A MDA meta-hierarchy divides a model into three layers. Therefore this approach is able to validate partial models using Alloy. Validating partial models reduce execution time. For an example of realistic validation, this paper shows application to the specification of an information control system modeling language and results of the validations for the specification., IEEE
Asia-Pacific Conference on Computer Aided System Engineering (APCASE) 2014, Feb. 2014,
[] 離散構造化モデル記述言語系OOJの構築と効果的な利用法,---分析からプログラムまでの一貫開発とV&V評価実現の検討---
Masayuki Hatakeyama; Yosuke Ikeda; Keisuke Mitsuduka; Mikio Ohki; Kazuo Katohgi; Yoshikazu Ueda
情報処理学会論文誌:数理モデル化と応用, Dec. 2013, []
UMLとの比較に基づくオブジェクト指向分析設計記述言語OONJの評価
Yosuke Ikeda; Mikio Ohki; Keisuke Mitsuduka; Yoshikazu Ueda; Kazuo Katohgi; Masayuki Hatakeyama
情報処理学会論文誌:数理モデル化と応用, Sep. 2012, []
情報制御システム記述言語による列車運行制御モデルの記述と検証
Kei Kogai; Kyohei Oyama; Yoshikazu Ueda; Yuhki Takahashi; Takayuki Takezawa; Toshihiko Nakano
日本ソフトウェア科学会コンピュータソフトウェア, Aug. 2012, []
Co-Analysis of SysML and Simulink Models for Cyber-Physical Systems DesignShin Nakajima; Satoru Furukawa; Yoshikazu Ueda, Model-Based Development (MBD) is a promising approach to achieving the required reliability levels of Cyber-Physical Systems. These systems are inherently heterogeneous. For example, models such as a controller and a plant have different characteristics. This paper proposes a Co-Analysis method. Logic-based analysis is employed to deal with an under-constrained or non-deterministic controller described with SysML. The analysis of the plant with Simulink adapts numerical simulation methods since the model represents physical phenomena whose time-dependent behavior is deterministic but computed with the initial states. The paper discusses further issues with the proposed co-analysis method. © 2012 IEEE.
IEEE 18th International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA 2012), Aug. 2012,
[] Alloyを利用した情報制御システム記述言語の仕様検証の実用化
Kei Kogai; Yoshikazu Ueda; Satoshi Ohkubo; Yuhki Nakano; Toshihiko Nakano
日本ソフトウェア科学会コンピュータソフトウェア, Nov. 2010, []
A Study of Quality Evaluation Model for UML Design
佐藤 美穂; 田村 真吾; 上田 賀一
Transactions of Information Processing Society of Japan, Jul. 2008, []
Object-oriented Program Design Description Language OOPD and Its Description Environment.
Kazuo Katougi; Masayuki Hatakeyama; Yoshikazu Ueda
Transactions of Information Processing Society of Japan, May 2002
A Programming Language for Object-oriented concurrent System Design.
平井 譲; 上田 賀一
Transaction of Information Processing Society of Japan, 2000
メタ階層アーキテクチャにおけるモデル生成・解釈機構の開発
Ryuichi Shouji; Yoshikazu Ueda
JSSST, Foundation of Software Engineering, 1999, []
並列オブジェクト指向シミュレーションのための記述言語とプログラム設計
Yuzuru Hirai; Kei Kogai; Yoshikazu Ueda
JSSST, Foundation of Software Engineering, 1998, []
Supporting System for Acquiring Requirement and Deriving Specification from Descriptions Using Natural Language.
Yozo Takizawa; Yoshikazu Ueda
Transactions of Information Processing Society of Japan, 1997
メタ階層に基づくモデルベースソフトウェア開発基盤の提案
Yoshikazu Ueda; Sonomi Anma; Daisuke Takahashi
JSSST, Foundation of Software Engineering, 1996, []
Derivation Supporting System of Object-Oriented Requirement Specification
Yozo Takizawa; Yoshikazu Ueda
JSSST, Foundations of Software Engineering, 1994, []
Description Language based on Class Version and Relationship
Hideto Shimura; Yoshikazu Ueda
JSSST,Foundations of Software Engineering, 1994
Improved Complex Demodulation Method for Frequency Analysis.
郝 英利; 上田 賀一; 石井 直宏
電子情報通信学会論文誌(DII), 1989
Automatic Detection Methods of Spindle Waves in Sleep EEG.
上田 賀一; 郝 英利; 石井 直宏
電子情報通信学会論文誌(DII), 1989
Estimation for Spread Forms of Spindle Waves in Multi-chamel EEG
Yoshikazu Ueda; Naohiro Ishii
電子情報通信学会論文誌(D), 1988
