ディペンダブルソフトウェア工学 中島研究室

Japanese | English

研究成果

[2013] [2012] [2011] [2010] [2009] [2008] [2007] [2006 -]

(日本語と英語による主要な研究成果)


2013

書籍

  1. ソフト・エッジ -ソフトウェア開発の科学を求めて-
    中島 震、みわよしこ(著)
    丸善出版  2013.3  ISBN: 978-4-621-05383-6

論文

  1. 実行時干渉の発生確率予測
    中島 震
    コンピュータソフトウェア 30(3), 2013.8
  2. 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
  3. 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

書籍

  1. 形式手法入門 -ロジックによるソフトウェア設計-
    中島 震(著)
    オーム社  2012.4  ISBN: 978-4-274-21188-1

論文

  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
  2. Importance Sampling of Runtime Interference
    Shin Nakajima
    Proc. of 19th Asia-Pacific Software Engineering Conference (APSEC 2012), 2012.12
  3. 自己適応Webアプリケーションシステム:概念アーキテクチャと実現フレームワーク
    中島 震
    コンピュータソフトウェア 29(3), 2012.8
  4. 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
  5. ソフトウェアモデル検査とテストケース生成の統合
    橋本 祐介, 中島 震
    情報処理学会論文誌 53(2) 548-556, 2012.2

2011

書籍

  1. オープン・イノベーション・システム ~欧州における自動車組込みシステムの開発と標準化~
    徳田 昭雄、立本 博文、小川 紘一(編著) (担当範囲:第5章(共著)、付録1)
    晃洋書房  2011.7  ISBN:978-4-7710-2287-4
  2. 抽象によるソフトウェア設計-Alloyではじめる形式手法-
    D. Jackson (著)、中島 震 (監訳)、今井 健男、酒井 政裕、遠藤 侑介、片岡 欣夫 (訳)
    オーム社  2011.7  ISBN:978-4-274-06858-4

論文

  1. 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
  2. An Architecture of Dynamically Adaptive PHP-based Web Applications
    Shin Nakajima
    Proc. of 18th Asia-Pacific Software Engineering Conference (APSEC 2011), 2011.12
  3. 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
  4. 有界モデル検査法を用いたCプログラムのモジュラー検証
    橋本 祐介, 中島 震
    情報処理学会論文誌 52(8), 2011.8
  5. 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)
  6. 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

書籍

  1. SPINモデル検査入門
    M. Ben-Ari(著)、中島 震(監訳)、谷津 弘一、野中 哲、足立 太郎(訳)
    オーム社  2010.3  ISBN:978-4-274-20844-7

解説

  1. ソフトウェア品質確保の技術動向
    中島震
    自動車研究 32(10) 561-565 2010.10
  2. From Counterexamples to Incremental Interactive Tracing of Errors
    Franz Weitl, Shin Nakajima, and Burkhard Freitag
    it - Information Technology 52(5) 295-297 2010.9

論文

  1. 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
  2. Reusable aspect components for Web applications
    Keiji Hokamura, Naoyasu Ubayashi, Shin Nakajima, and Akihito Iwai
    Proc. IEEE TENCON 2010 2010.11
  3. 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
  4. 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
  5. 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
  6. 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
  7. 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
  8. 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
  9. 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
  10. Semi-Automated Debugging of FODA Feature Diagrams
    S. Nakajima
    Proc. ACM/SAC 2010  2010.3

2009

書籍

  1. ソフトウェア工学の基礎 XVI
    中島震、鷲崎弘宜(編)
    近代科学社  2009.11  ISBN:978-4-7649-0376-0
  2. Proceedings of ISORC 2009
    Shin NAKAJIMA et al (eds.)
    IEEE  2009.3

解説

  1. Alloy : 自動解析可能なモデル規範型形式仕様言語
    中島 震、鵜林 尚靖
    コンピュータソフトウェ 26(3) 78-83 2009.10

論文

  1. 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
  2. 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
  3. Modular Checking with Model Checking
    Y. Hashimoto and S. Nakajima
    Electronic Notes in Theoretical Computer Science (ENTCS) 254 105-122 2009.10
  4. Constructing FODA Feature Diagrams with a GUI-based Tool
    S. Nakajima
    Proc. SEKE 2009 20-25 2009.7
  5. 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

書籍

  1. SPINモデル検査:検証モデリング技法
    中島 震
    近代科学社  2008.4  ISBN:978-4-7649-0353-1

解説

  1. 形式手法の潮流 : アーキテクチャへの関心
    中島 震
    システム/制御/情報 : システム制御情報学会誌 52(9) 310-315 2008.9

論文

  1. 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

書籍

  1. Bメソッドによる形式仕様記述
    中島 震(監修)、来間 啓伸(著)
    近代科学社 2007.12 ISBN:978-4-764-90347-0

解説

  1. ソフトウェア工学の道具としての形式手法
    中島 震
    NII TR-2007-007J, 2007.7
    [online]
  2. プログラム簡易検証ツールESC/Java2
    中島 震
    コンピュータソフトウェア 24(2) 2-7 2007.4
  3. 仕様記述言語Zと証明環境Isabelle/HOL-Z
    来間 啓伸, B. Wolff, D. Basin, 中島 震
    コンピュータソフトウェア 24(2) 21-26 2007.4

論文

  1. Light-weight Formal Analysis of FODA Feature Diagrams
    S. Nakajima and N. Ubayashi
    Proc. 4th RISE, 2007.11
  2. 代数仕様言語Maudeを用いた制約オートマトンの実現
    中島 震
    情報処理学会論文誌 48(10) 3341-3351, 2007.10
  3. コンテキストベース・プロダクトライン開発とVDM++の適用
    鵜林尚靖, 金川太俊, 瀬戸敏喜, 中島震, 平山雅之
    情報処理学会論文誌 48(8) 2492-2507, 2007.8
  4. 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

解説

  1. モデル検査法のソフトウェア開発への応用
    中島 震
    コンピュータ・ソフトウェア 23(2) 72-86 2006.4

論文

  1. Aspect-Oriented Software Design with a Variant of UML/STD
    S. Nakajima and T. Tamai
    Proc. SCESM 2006 44-50, 2006.5
  2. Model-Checking Behavioral Specifications of BPEL Applications
    S. Nakajima
    Electronic Notes in Theoretical Computer Science (ENTCS) 151-2, 89-105, 2006.5

2005

論文

  1. UMLステートダイアグラムの亜種を用いた組み込みソフトウェア振舞い解析
    中島 震
    情報処理学会論文誌 46(11) 2643-2653 2005.11
  2. Lightweight Formal Analysis of Web Service Flows
    S. Nakajima
    Progress in Informatics No.2, 57-76 2005.11
    [online]
  3. ユビキタスアプリケーション向け移動エージェントの相互運用
    長谷川哲夫,長健太,大須賀明彦,粂野文洋,中島震,本位田真一
    電気学会論文誌(C) 125(8) 1296-1304 2005.8
  4. 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

解説

  1. 組み込みソフトウェアのモデル検査技術入門
    中島 震
    情報処理 45(7) 690-693, 2004.7
  2. 書評 - The SPIN Model Checker
    中島 震
    コンピュータソフトウェア 21(2) 61-69 2004.3

論文

  1. 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
  2. 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
  3. コンポーネントフレームワーク振舞い解析への多値遷移システムの応用
    中島 震
    コンピュータ・ソフトウェア 21(2) 32-36, 2004.3

2003

論文

  1. 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
  2. Webサービスフロー記述のモデル検査検証
    中島 震
    情報処理学会論文誌 44(3) 942-952, 2003.3

2002

書籍

  1. オブジェクト指向最前線2002
    中島 震、三ツ井 欽一(編)
    近代科学社 2002.9 ISBN:978-4-764-90302-9

論文

  1. Behavioural Analysis of Component Framework with Multi-Valued Transition Systems
    S. Nakajima
    Proc. APSEC 2002 217-226, 2002.12
  2. Verification of Web Services Flows with Model-Checking Techniques
    S. Nakajima
    Proc. Cyber World 2002, 378-385, 2002.11
  3. アプリケーションシステム開発のための移動エージェントの定量的評価
    前田 直人, 中島 震
    情報処理学会論文誌 42(7) 2330-2339, 2002.7
  4. EJBコンポーネントアーキテクチャのSPINによる振舞い解析
    中島震, 玉井 哲雄
    コンピュータ・ソフトウェア 19(2) 2-18, 2002.3
    「日本ソフトウェア科学会論文賞受賞」
  5. 問題領域向けトランスレータ構築支援ツールキット
    登内 敏夫, 中島 震
    情報処理学会論文誌 43(1) 146-155, 2002.1

2001

解説

  1. オジェクト指向デザインと形式手法
    中島 震
    コンピュータ・ソフトウェア 18(5) 17-46, 2001.9

論文

  1. Management of Script Evolution with Mobile Agent Technology
    S. Nakajima
    Proc. IWPSE 2001, 2001.9
  2. Behavioural Analysis of the Enterprise JavaBeans Component Architecture
    S. Nakajima and T. Tamai
    Proc. SPIN 2001 163-182, 2001.5

2000

Ph.D.学位論文

  1. An Algebraic Approach to Object-Oriented Software Engineering
    Shin Nakajima
    The University of Tokyo 2000.11

解説

  1. 書評 - Objects, Components and Frameworks with UML
    中島 震
    コンピュータソフトウェア 17(6) 86-90 2000.11

論文

  1. 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
  2. 装置組み込み用高速Q3エージェントプラットフォームの実現
    登内 敏夫, 中島 震
    情報処理学会論文誌 41(4) 1226-1233, 2000.4
  3. Aspect-Centered Design of Object-Oriented Frameworks
    Shin Nakajima
    Trans. IPSJ 41(3) 758-766, 2000.3

1999

論文

  1. Using Algebraic Specification Techniques in Development of Object-Oriented Frameworks
    S. Nakajima
    Proc. World Congress on Formal Methods (FM'99) 1664-1683, 1999.9
  2. CafeOBJによるODPトレーダ仕様の記述
    中島 震, 二木 厚吉
    コンピュータ・ソフトウェア 16(4) 76-79, 1999.7
  3. 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

論文

  1. 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
  2. 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
  3. 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
  4. An Object-Oriented Modeling Method for Algebraic Specifications in CafeOBJ
    S. Nakajima and K. Futatsugi
    Proc. IEEE/ACM ICSE'97 34-44, 1997.5
  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

論文

  1. 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

論文

  1. 組み合わせオブジェクトに基づくGUIライブラリ
    登内 敏夫, 中島 震
    コンピュータ・ソフトウェア 12(3) 49-58, 1995.5
  2. オブジェクトの集団的振舞いの設計と検証のための高レベルペトリネット
    元木 誠, 中島 震
    情報処理学会論文誌 36(5) 1163-1172, 1995.5
  3. GILO/Z : オブジェクト指向仕様記述のためのZ記法の拡張
    中島 震
    情報処理学会論文誌 36(5) 1059-1069, 1995.5

1994

解説

  1. NECにおけるオブジェクト指向技術への取り組み
    宮下 洋一, 中島 震
    NEC技報 47(6) 3-8, 1994.6

1989

論文

  1. 制約伝播機構を内蔵するオブジェクト指向言語 : COOL
    中島 震
    情報処理学会論文誌 30(1) 101-108, 1989.1

1984

論文

  1. MONJU: Constraint-Keeping Object-Oriented Language
    S. Nakajima, S., K. Ohmori, and H. Horita
    Proc. IEEE COMPSAC'84 232-239, 1984.11