機能安全対応基盤ソフト向け階層型検証システムアーキテクチャ
成沢 文雄,上田 賀一, ラスト(シニア)オーサー, 自動車技術会
自動車技術会論文集, 2019年03月25日, ［査読有り］

Safety verification method for priority-based real-time software
Fumio 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年, ［査読有り］

組込みシステム検査のための協調解析　　　　　　　　　　　　　　　
古川 覚; 上田 賀一; 中島 震, 責任著者
日本ソフトウェア科学会コンピュータソフトウェア, 2014年08月, ［査読有り］

Realistic Validation of Specification for Modeling Language using Alloy
Kei 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, 2014年02月, ［査読有り］

離散構造化モデル記述言語系OOJの構築と効果的な利用法,---分析からプログラムまでの一貫開発とV&V評価実現の検討---　　　　　　　　　　　　　　　
畠山 正行; 池田 陽祐; 三塚 恵嗣; 大木 幹生; 加藤木 和夫; 上田 賀一
情報処理学会論文誌:数理モデル化と応用, 2013年12月, ［査読有り］

UMLとの比較に基づくオブジェクト指向分析設計記述言語OONJの評価　　　　　　　　　　　　　　　
池田 陽祐; 大木 幹生; 三塚 恵嗣; 上田 賀一; 加藤木 和夫; 畠山 正行
情報処理学会論文誌:数理モデル化と応用, 2012年09月, ［査読有り］

情報制御システム記述言語による列車運行制御モデルの記述と検証　　　　　　　　　　　　　　　
小飼 敬; 小山 恭平; 上田 賀一; 高橋 勇喜; 武澤隆之; 中野 利彦, 責任著者
日本ソフトウェア科学会コンピュータソフトウェア, 2012年08月, ［査読有り］

Co-Analysis of SysML and Simulink Models for Cyber-Physical Systems Design
Shin 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), 2012年08月, ［査読有り］

Alloyを利用した情報制御システム記述言語の仕様検証の実用化　　　　　　　　　　　　　　　
小飼敬; 上田賀一; 大久保訓; 高橋勇喜; 中野利彦, 責任著者
日本ソフトウェア科学会コンピュータソフトウェア, 2010年11月, ［査読有り］

UML設計を対象とした品質評価モデルの検討　　　　　　　　　　　　　　　
佐藤 美穂; 田村 真吾; 上田 賀一, 責任著者
情報処理学会論文誌, 2008年07月, ［査読有り］

オブジェクト指向プログラム設計記述言語OOPDとその記述環境　　　　　　　　　　　　　　　
加藤木 和夫; 畠山 正行; 上田 賀一
情報処理学会論文誌, 2002年05月

並行システムのオブジェクト指向設計に適したプログラミング言語の開発　　　　　　　　　　　　　　　
平井 譲; 上田 賀一, 責任著者
情報処理学会論文誌, 2000年

メタ階層アーキテクチャにおけるモデル生成・解釈機構の開発　　　　　　　　　　　　　　　
庄司龍一; 上田賀一, 責任著者
日本ソフトウェア科学会 ソフトウェア工学の基礎, 1999年, ［査読有り］

並列オブジェクト指向シミュレーションのための記述言語とプログラム設計　　　　　　　　　　　　　　　
平井譲; 小飼敬; 上田賀一, 責任著者
日本ソフトウェア科学会 ソフトウェア工学の基礎, 1998年, ［査読有り］

自然言語記述による要求仕様導出支援システムの提案　　　　　　　　　　　　　　　
滝沢 陽三; 上田 賀一, 責任著者
情報処理学会論文誌, 1997年

メタ階層に基づくモデルベースソフトウェア開発基盤の提案　　　　　　　　　　　　　　　
上田賀一; 安間その美; 高橋大輔, 筆頭著者
日本ソフトウェア科学会 ソフトウェア工学の基礎, 1996年, ［査読有り］

オブジェクト指向概念に基づく要求仕様の導出支援システム　　　　　　　　　　　　　　　
滝沢 陽三; 上田 賀一, 責任著者
日本ソフトウェア科学会 ソフトウェア工学の基礎, 1994年, ［査読有り］

クラスバージョンと関係に基づく記述モデル　　　　　　　　　　　　　　　
志村 秀人; 上田賀一, 責任著者
日本ソフトウェア科学会 ソフトウェア工学の基礎, 1994年

周波数解析のためのComplex Demodulation法の改良　　　　　　　　　　　　　　　
郝 英利; 上田 賀一; 石井 直宏
電子情報通信学会論文誌(DII), 1989年

睡眠脳波解析における紡錘波の自動検出法　　　　　　　　　　　　　　　
上田 賀一; 郝 英利; 石井 直宏, 筆頭著者
電子情報通信学会論文誌(DII), 1989年

多チャネル脳波における睡眠紡錘波の出現形態の推定　　　　　　　　　　　　　　　
上田 賀一; 石井 直宏, 筆頭著者
電子情報通信学会論文誌(D), 1988年

Detecting Defects in Object Oriented Designs Using Design Metrics
C.Munkhnasan; Y.Ueda
Joint Conference on Knowledge Based Software Engineering 2006, 2006年
ラスト(シニア)オーサー

ソフトウェアリポジトリ構築のためのファセット分類アプローチ
上田 賀一; 久保田 深雪
茨城大学工学部研究集報, 2002年
筆頭著者

オブジェクトベース言語Brambleにおける形式的型検査
上田 賀一; 原田 哲也
茨城大学工学部研究集報, 2001年
筆頭著者

ソフトシステム方法論に基づくソフトウェア開発法と開発事例
上田 賀一; 平井 譲; 武野内 康寛; 大島 俊泰
茨城大学工学部研究集報, 1999年
筆頭著者

オブジェクト指向開発法によるグループウェア開発基盤モデルの提案
上田 賀一; 山田 由紀
茨城大学工学部研究集報, 1995年
筆頭著者

メタモデルに基づくプロセスモデルの記述と実行
上田 賀一; 安間 その美; 志村 秀人
茨城大学工学部研究集報, 1994年
筆頭著者

ファイル間の関係に基づく視覚的なファイル管理
上田 賀一; 秋山 憲一; 山田 裕二
茨城大学工学部研究集報, 1993年
筆頭著者

睡眠脳波中の紡錘波の挙動と心拍のゆらぎの抽出
上田 賀一; 石井 直宏
日本ME学会雑誌BME, 1993年
筆頭著者

ファジィ応用のためのプログラミング言語の設計とプログラミング支援環境
上田 賀一
茨城大学工学部研究集報, 1991年

オブジェクト指向システム分析 ---３つのモデルに基づくアプローチ---　　　　　　　　　　　　　　　
東京電機大学出版局, 1993年

SimulinkとSMTソルバの連携による協調解析支援ツールの開発　　　　　　　　　　　　　　　
Engielista Anak Norman,上田 賀一
電子情報通信学会，技術報告(知能ソフトウェア工学研究会), 2023年03月17日

OSSプロジェクトの早期成否判別に関する活動情報の調査　　　　　　　　　　　　　　　
菊池 悠雅,上田 賀一
電子情報通信学会，技術報告(知能ソフトウェア工学研究会), 2023年03月17日

POIとGEOを組み合わせた人間活動の類似性予測法の検討　　　　　　　　　　　　　　　
曹 慶荥,上田 賀一
電子情報通信学会，技術報告(ライフインテリジェンスとオフィス情報システム研究会), 2021年03月04日

検証性質を充足する解空間の可視化による協調解析支援ツールの開発　　　　　　　　　　　　　　　
兎澤 佑; 上田 賀一
情報処理学会, 研究報告(ソフトウェア工学), 2015年03月

SysMLモデルの制約妥当性検証に関する考察　　　　　　　　　　　　　　　
加藤 秀明; 上田 賀一; 中島 震
情報処理学会, 組込みシステムシンポジウム2010, 2010年10月28日

Simulink に基づくテストファーストUML設計手法の提案　　　　　　　　　　　　　　　
原 彬寛; 吉田 聡; 上田 賀一; 中島 震
情報処理学会, 組込みシステムシンポジウム2008, 2008年10月31日

UMLによる組込みソフトウェア設計のレビュー支援ツールの開発　　　　　　　　　　　　　　　
鈴木 健司; 上田 賀一
情報処理学会, 組込みシステムシンポジウム2007, 2007年10月19日

Detecting Defects in Object Oriented Designs Using Design Metrics　　　　　　　　　　　　　　　
Munkhnasan Choinzon; Yoshikazu Ueda
Joint Conference On Knowledge-Based Software Engineering 2006 (JCKBSE'06), 2006年08月28日

IEEE, Computer Society

米国計算機学会(Association for Computing Machinery)

日本ソフトウェア科学会

情報処理学会

電子情報通信学会