研究成果
[2013]
[2012]
[2011] [2010] [2009] [2008] [2007] [2006 -]
(日本語と英語による主要な研究成果)
2013
書籍
- ソフト・エッジ -ソフトウェア開発の科学を求めて-
中島 震、みわよしこ(著)
丸善出版 2013.3 ISBN: 978-4-621-05383-6
論文
- 実行時干渉の発生確率予測
中島 震
コンピュータソフトウェア 30(3), 2013.8
- Inductive Verification of Hybrid Automata with Strongest Postcondition Calculus
Daisuke Ishii, Guillaume Melquiond, and Shin Nakajima
Proc. of 10th International Conference on integrated Formal Methods (iFM 2013), 2013.6
- Efficient Online Analysis of Accidental Fault Localization for Dynamic Systems using Hidden Markov Model
Ning Ge, Shin Nakajima, and Marc Pantel
Proc. TMS/DEVS 2013, 2013.4
2012
書籍
- 形式手法入門 -ロジックによるソフトウェア設計-
中島 震(著)
オーム社 2012.4 ISBN: 978-4-274-21188-1
論文
- A formal approach to testing programs in practice
Shaoying Liu, Wuwei Shen, and Shin Nakajima
Comput. Sci. Inf. Syst. 9(4): 1469-1491, 2012.12
- Importance Sampling of Runtime Interference
Shin Nakajima
Proc. of 19th Asia-Pacific Software Engineering Conference (APSEC 2012), 2012.12
- 自己適応Webアプリケーションシステム:概念アーキテクチャと実現フレームワーク
中島 震
コンピュータソフトウェア 29(3), 2012.8
- Co-analysis of SysML and Simulink Models for Cyber-Physical Systems Design
Shin Nakajima, Satoru Furukawa, and Yoshikazu Ueda
Proc. RTCSA 2012, 473-478, 2012.8
- ソフトウェアモデル検査とテストケース生成の統合
橋本 祐介, 中島 震
情報処理学会論文誌 53(2) 548-556, 2012.2
2011
書籍
- オープン・イノベーション・システム ~欧州における自動車組込みシステムの開発と標準化~
徳田 昭雄、立本 博文、小川 紘一(編著) (担当範囲:第5章(共著)、付録1)
晃洋書房 2011.7 ISBN:978-4-7710-2287-4
- 抽象によるソフトウェア設計-Alloyではじめる形式手法-
D. Jackson (著)、中島 震 (監訳)、今井 健男、酒井 政裕、遠藤 侑介、片岡 欣夫 (訳)
オーム社 2011.7 ISBN:978-4-274-06858-4
論文
- A "Vibration" Method for Automatically Generating Test Cases Based on Formal Specifications
Shaoying Liu and Shin Nakajima
Proc. of 18th Asia-Pacific Software Engineering Conference (APSEC 2011), 2011.12
- An Architecture of Dynamically Adaptive PHP-based Web Applications
Shin Nakajima
Proc. of 18th Asia-Pacific Software Engineering Conference (APSEC 2011), 2011.12
- Integrated Model Checking of Static Structure and Dynamic Behavior using Temporal Description Logics
Franz Weitl and Shin Nakajima
Proc. of 11th International Workshop on Automated Verification of Critical Systems (AVoCS 2011), 2011.9
- 有界モデル検査法を用いたCプログラムのモジュラー検証
橋本 祐介, 中島 震
情報処理学会論文誌 52(8), 2011.8
- A Framework for Integrating Formal Specification, Review, and Testing to Enhance Software Reliability
Shaoying Liu, Tetsuo Tamai, and Shin Nakajima
International Journal of Software Engineering and Knowledge Engineering 21(2): 259-288 (2011)
- Utilizing Model Checking for Automatic Test Case Generation from Conjunctions of Atomic Predicate Expressions
Cong Tian, Shaoying Liu, and Shin Nakajima
Proc. of 3rd Workshop on Constraints in Software Testing, Verification, and Analysis 2011.3
2010
書籍
- SPINモデル検査入門
M. Ben-Ari(著)、中島 震(監訳)、谷津 弘一、野中 哲、足立 太郎(訳)
オーム社 2010.3 ISBN:978-4-274-20844-7
解説
- ソフトウェア品質確保の技術動向
中島震
自動車研究 32(10) 561-565 2010.10
-
From Counterexamples to Incremental Interactive Tracing of Errors
Franz Weitl, Shin Nakajima, and Burkhard Freitag
it - Information Technology 52(5) 295-297 2010.9
論文
-
Detecting feature interferences in PHP-based Web applications
Shin Nakajima
Proceedings of 22nd International Conference on Software & Systems Engineering and their Applications (ICSSEA 2010) 2010.12
-
Reusable aspect components for Web applications
Keiji Hokamura, Naoyasu Ubayashi, Shin Nakajima, and Akihito Iwai
Proc. IEEE TENCON 2010 2010.11
-
Rewriting Logic Approach to Modeling and Analysis of Client Behavior in Open Systems
Shin Nakajima, Masaki Ishiguro, ans Kazuyuki Tanaka
Proc. 8th IFIP Workshop on Software Technologies for Future Embedded and Ubiquitous Systems (SEUS 2010) 83-94 2010.10
-
Automatic Transformation from Formal Specifications to Functional Scenario Forms for Automatic Test Case Generation
S. Liu, T. Hayashi, K. Takahashi, K. Kimura, T. Nakayama, and S. Nakajima
Proc. 9th International Conference on Software Methodologies, Tools and Techniques (SoMet 2010) 2010.10
-
Structured Counterexamples for the Temporal Description Logic ALCCTL
Franz Weitl, Shin Nakajima and Burkhard Freitag
Proceedings of 8th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2010) 232-243 2010.9
-
Non-clausal Encoding of Feature Diagram for Automated Diagnosis
Shin Nakajima
Proceedings of 14th International Software Product Line Conference (SPLC 2010) 420-424 2010.9
-
Context-dependent Product Line Practice for Constructing Reliable Embedded Systems
Naoyasu Ubayashi, Shin Nakajima, and Masayuki Hirayama
Proceedings of 14th International Software Product Line Conference (SPLC 2010) 1-15 2010.9
-
Incremental Construction of Counterexamples in Model Checking Web Documents
Franz Weitl and Shin Nakajima
Proceedings of 6th International Workshop on Automated Specification and Verification of Web Systems 2010.7
-
A Decompositional Approach to Automatic Test Case Generation Based on Formal Specifications
Shaoying Liu and Shin Nakajima
Proceedings of IEEE International Conference on Secure Software Integration and Reliability Improvement (ICSSIRI 2010) 147-155 2010.6
- Semi-Automated Debugging of FODA Feature Diagrams
S. Nakajima
Proc. ACM/SAC 2010 2010.3
2009
書籍
- ソフトウェア工学の基礎 XVI
中島震、鷲崎弘宜(編)
近代科学社 2009.11 ISBN:978-4-7649-0376-0
- Proceedings of ISORC 2009
Shin NAKAJIMA et al (eds.)
IEEE 2009.3
解説
- Alloy : 自動解析可能なモデル規範型形式仕様言語
中島 震、鵜林 尚靖
コンピュータソフトウェ 26(3) 78-83 2009.10
論文
- A Guidance and Methodology for Employing Model-Checking for Software Development
M. Ishiguro, K. Tanaka, A. Umemura, S. Nakajima, and T. Kishi
Proc. APESER 2009 2009.12
- Modular Checking of C Programs using SAT-based Bounded Model-Checker
Y. Hashimoto and S. Nakajima
Proc. 16th Asia-Pacific Software Engineering Conference (APSEC 2009) 2009.12
- Modular Checking with Model Checking
Y. Hashimoto and S. Nakajima
Electronic Notes in Theoretical Computer Science (ENTCS) 254 105-122 2009.10
- Constructing FODA Feature Diagrams with a GUI-based Tool
S. Nakajima
Proc. SEKE 2009 20-25 2009.7
-
Integration of Formal Specification, Review, and Testing for Software Component Quality Assurance
S. Liu, T. Tamai, and S. Nakajima
Proceedings of SAC 2009 415-421 2009.3
2008
書籍
- SPINモデル検査:検証モデリング技法
中島 震
近代科学社 2008.4 ISBN:978-4-7649-0353-1
解説
- 形式手法の潮流 : アーキテクチャへの関心
中島 震
システム/制御/情報 : システム制御情報学会誌 52(9) 310-315 2008.9
論文
- Aspect-Oriented Programming for Web Controller Layer
Keiji Hokamura, Naoyasu Ubayashi, Shin Nakajima and Akihito Iwai
Proc. 15th Asia-Pacific Software Engineering Conference (APSEC 2008) 529-536 2008.12
2007
書籍
- Bメソッドによる形式仕様記述
中島 震(監修)、来間 啓伸(著)
近代科学社 2007.12 ISBN:978-4-764-90347-0
解説
- ソフトウェア工学の道具としての形式手法
中島 震
NII TR-2007-007J, 2007.7
[online]
-
プログラム簡易検証ツールESC/Java2
中島 震
コンピュータソフトウェア 24(2) 2-7 2007.4
-
仕様記述言語Zと証明環境Isabelle/HOL-Z
来間 啓伸, B. Wolff, D. Basin, 中島 震
コンピュータソフトウェア 24(2) 21-26 2007.4
論文
- Light-weight Formal Analysis of FODA Feature Diagrams
S. Nakajima and N. Ubayashi
Proc. 4th RISE, 2007.11
- 代数仕様言語Maudeを用いた制約オートマトンの実現
中島 震
情報処理学会論文誌 48(10) 3341-3351, 2007.10
- コンテキストベース・プロダクトライン開発とVDM++の適用
鵜林尚靖, 金川太俊, 瀬戸敏喜, 中島震, 平山雅之
情報処理学会論文誌 48(8) 2492-2507, 2007.8
-
Context-aware Feature-Oriented Modeling with an Aspect Extension of VDM
N. Ubayashi and S. Nakajima
Proc. ACM SAC 2007 1269-1274, 2007.3
2006
解説
- モデル検査法のソフトウェア開発への応用
中島 震
コンピュータ・ソフトウェア 23(2) 72-86 2006.4
論文
- Aspect-Oriented Software Design with a Variant of UML/STD
S. Nakajima and T. Tamai
Proc. SCESM 2006 44-50, 2006.5
-
Model-Checking Behavioral Specifications of BPEL Applications
S. Nakajima
Electronic Notes in Theoretical Computer Science (ENTCS) 151-2, 89-105, 2006.5
2005
論文
-
UMLステートダイアグラムの亜種を用いた組み込みソフトウェア振舞い解析
中島 震
情報処理学会論文誌 46(11) 2643-2653 2005.11
-
Lightweight Formal Analysis of Web Service Flows
S. Nakajima
Progress in Informatics No.2, 57-76 2005.11
[online]
- ユビキタスアプリケーション向け移動エージェントの相互運用
長谷川哲夫,長健太,大須賀明彦,粂野文洋,中島震,本位田真一
電気学会論文誌(C) 125(8) 1296-1304 2005.8
-
Highly Reliable Embedded Software Development Using Advanced Software Technologies
T.Katayama, T.Nakajima, T.Yuasa, T.Kishi, S.Nakajima, S.Oikawa, M.Yasugi, T.Aoki, M.Okazaki, and S. Umatani
The IEICE Transactions on Information and Systems 2005.6
2004
解説
- 組み込みソフトウェアのモデル検査技術入門
中島 震
情報処理 45(7) 690-693, 2004.7
-
書評 - The SPIN Model Checker
中島 震
コンピュータソフトウェア 21(2) 61-69 2004.3
論文
-
Model-Checking of Safety and Security Aspects in Web Service Flows
S. Nakajima
Proc. International Conference on Web Engineering (ICWE 2004) 488-501, 2004.7
-
Project Report: High Reliable Object-Oriented Embedded Software Design
T. Kishi, T. Aoki, S. Nakajima, N. Noda, and T. Katayama
Proc. IEEE WSTFEUS'04 144-148, 2004.5
-
コンポーネントフレームワーク振舞い解析への多値遷移システムの応用
中島 震
コンピュータ・ソフトウェア 21(2) 32-36, 2004.3
2003
論文
- Interoperability for mobile agents by incarnation agents
T. Hasegawa, K. Cho, F. Kumeno, S. Nakajima, A. Ohsuga, S. Honiden
Proc. AAMAS 2003, 1006-1007, 2003.7
- Webサービスフロー記述のモデル検査検証
中島 震
情報処理学会論文誌 44(3) 942-952, 2003.3
2002
書籍
- オブジェクト指向最前線2002
中島 震、三ツ井 欽一(編)
近代科学社 2002.9 ISBN:978-4-764-90302-9
論文
- Behavioural Analysis of Component Framework with Multi-Valued Transition Systems
S. Nakajima
Proc. APSEC 2002 217-226, 2002.12
-
Verification of Web Services Flows with Model-Checking Techniques
S. Nakajima
Proc. Cyber World 2002, 378-385, 2002.11
- アプリケーションシステム開発のための移動エージェントの定量的評価
前田 直人, 中島 震
情報処理学会論文誌 42(7) 2330-2339, 2002.7
- EJBコンポーネントアーキテクチャのSPINによる振舞い解析
中島震, 玉井 哲雄
コンピュータ・ソフトウェア 19(2) 2-18, 2002.3
「日本ソフトウェア科学会論文賞受賞」
- 問題領域向けトランスレータ構築支援ツールキット
登内 敏夫, 中島 震
情報処理学会論文誌 43(1) 146-155, 2002.1
2001
解説
- オジェクト指向デザインと形式手法
中島 震
コンピュータ・ソフトウェア 18(5) 17-46, 2001.9
論文
-
Management of Script Evolution with Mobile Agent Technology
S. Nakajima
Proc. IWPSE 2001, 2001.9
-
Behavioural Analysis of the Enterprise JavaBeans Component Architecture
S. Nakajima and T. Tamai
Proc. SPIN 2001 163-182, 2001.5
2000
Ph.D.学位論文
-
An Algebraic Approach to Object-Oriented Software Engineering
Shin Nakajima
The University of Tokyo 2000.11
解説
- 書評 - Objects, Components and Frameworks with UML
中島 震
コンピュータソフトウェア 17(6) 86-90 2000.11
論文
-
A Directory Server for Mobile Agent Interoperability
Y. Beppu, S. Nakajima, F. Kumeno, K. Cho, T. Hasegawa, and A. Ohsuga
Proc. IEEE EDOC 2000 144-148, 2000.9
-
装置組み込み用高速Q3エージェントプラットフォームの実現
登内 敏夫, 中島 震
情報処理学会論文誌 41(4) 1226-1233, 2000.4
-
Aspect-Centered Design of Object-Oriented Frameworks
Shin Nakajima
Trans. IPSJ 41(3) 758-766, 2000.3
1999
論文
-
Using Algebraic Specification Techniques in Development of Object-Oriented Frameworks
S. Nakajima
Proc. World Congress on Formal Methods (FM'99) 1664-1683, 1999.9
-
CafeOBJによるODPトレーダ仕様の記述
中島 震, 二木 厚吉
コンピュータ・ソフトウェア 16(4) 76-79, 1999.7
-
An Algebraic Approach to Specification and Analysis of the ODP Trader
S. Nakajima and K. Futatsugi
Trans. IPSJ 40(4) 1861-1873, 1999.4
1997
論文
-
A Scripting Language for Network Management Applications and its Related Tool
M. Miki, M. Tanaka, M. Tomobe, and S. Nakajima
Proc. IEEE GLOBECOM'97 1714-1718, 1997.11
-
An Implementation of Customizable Services with Java/ORB Integration
M. Tomono, A. Yamanaka, T. Tonouchi, and S. Nakajima
Proc. IEEE GLOBECOM'97 1719-1723, 1997.11
-
An Implementation of OSI Management Q3 Agent Platform for Subscriber Networks
T. Tonouchi, T. Fukushima, A. Manki, and S. Nakajima
Proc. IEEE ICC'97 889-893, 1997.6
-
An Object-Oriented Modeling Method for Algebraic Specifications in CafeOBJ
S. Nakajima and K. Futatsugi
Proc. IEEE/ACM ICSE'97 34-44, 1997.5
-
A HORB-based Network Management System
A. Yamanaka, S. Nakajima, M. Tomono, and T. Tonouchi
Proc. IFIP/IEEE ICODP/ICDP'97 99-109, 1997.5
1996
論文
-
Object-Oriented Development Methodology for Telecommunication Network Management Software
S. Nakajima, M. Tomobe, M. Miki, and H. Hayashi
Proc. IEEE GLOBECOM'96 665-669, 1996.11
1995
論文
- 組み合わせオブジェクトに基づくGUIライブラリ
登内 敏夫, 中島 震
コンピュータ・ソフトウェア 12(3) 49-58, 1995.5
- オブジェクトの集団的振舞いの設計と検証のための高レベルペトリネット
元木 誠, 中島 震
情報処理学会論文誌 36(5) 1163-1172, 1995.5
- GILO/Z : オブジェクト指向仕様記述のためのZ記法の拡張
中島 震
情報処理学会論文誌 36(5) 1059-1069, 1995.5
1994
解説
- NECにおけるオブジェクト指向技術への取り組み
宮下 洋一, 中島 震
NEC技報 47(6) 3-8, 1994.6
1989
論文
-
制約伝播機構を内蔵するオブジェクト指向言語 : COOL
中島 震
情報処理学会論文誌 30(1) 101-108, 1989.1
1984
論文
- MONJU: Constraint-Keeping Object-Oriented Language
S. Nakajima, S., K. Ohmori, and H. Horita
Proc. IEEE COMPSAC'84 232-239, 1984.11
© Nakajima Laboratory at National Institute of Informatics