Performance information

• Improvement of Multi-label kNN Classifier with Self-adjusting Memory Using a Punitive Model for Drifting Data Streams　　　　　　　　　　　　　　　
  Thinzar Tun; Yuichi Goto
  Lecture Notes in Computer Science, Volume：15432, First page：283, Last page：297, Feb. 2025, [Reviewed], [Last]
  English, International conference proceedings
  DOI：https://doi.org/10.1007/978-981-96-0695-5_23
  DOI ID：10.1007/978-981-96-0695-5_23, ORCID：178393991
• Improvement of a Forward Reasoning Engine FreeEnCal for Trust Reasoning　　　　　　　　　　　　　　　
  Yuichi Goto; Yasuaki Taga
  Communications in Computer and Information Science, Volume：2144, First page：250, Last page：261, Aug. 2024, [Reviewed], [Lead, Corresponding]
  English, International conference proceedings
  DOI：https://doi.org/10.1007/978-981-97-5937-8_21
  DOI ID：10.1007/978-981-97-5937-8_21, ORCID：165329780
• A Belief Revision Mechanism with Trust Reasoning based on Extended Reciprocal Logic for Multi-Agent Systems　　　　　　　　　　　　　　　
  Sameera Basit; Yuichi Goto
  Computer Networks & Communications, Volume：13, Number：4, First page：161, Last page：173, Feb. 2023, [Reviewed], [Corresponding]
  When an agent receives messages from other agents, it does belief revision. A belief revision includes, i) a trust reasoning process, i.e., it obtains new belief related to the messages, and deduces implicitly unknown beliefs from the obtained belief; ii) in the case of contradiction in the belief set, it resolves the contradiction. So, trust reasoning, and belief revision must be included in the decision-making process of an intelligent agent in multi-agent systems. Although a belief revision mechanism with trust reasoning is demanded to construct multi-agent systems, there is no such belief revision mechanism. We, therefore, present a belief revision mechanism with trust reasoning based on extended reciprocal logic for multi-agent systems.
  Academy and Industry Research Collaboration Center (AIRCC), English, International conference proceedings
  DOI：https://doi.org/10.5121/csit.2023.130413
  DOI ID：10.5121/csit.2023.130413
• An Extension of Formal Analysis Method with Reasoning for Anonymity　　　　　　　　　　　　　　　
  Yating Wang; Yuichi Goto
  Lecture Notes in Computer Science, Volume：12034, First page：53, Last page：64, Mar. 2020, [Reviewed], [Last]
  Formal analysis method with reasoning has been proposed as an alternative formal analysis method for cryptographic protocols. In the method, at first, analysts formalize the participant’s and attacker’s behaviors in order to carry out forward reasoning, then analysts check whether the logic formulas that represents security flaws of the target protocol exist or not in deduced logical formulas. However, the current method can deal with security flaws related to authentication, confidentiality, fairness, and non-repudiation, but not anonymity. This paper proposes an extension of formal analysis method with reasoning for dealing with security flaws related to anonymity. The paper also gives a case study with the proposed method in the Bolignano protocol. The result shows that the extension method is useful to detect security flaws related to anonymity.
  Springer, English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-030-42058-1_5
  DOI ID：10.1007/978-3-030-42058-1_5, ISSN：1611-3349, SCOPUS ID：85082401801
• An Extension of Reciprocal Logics for Trust Reasoning　　　　　　　　　　　　　　　
  Sameera Basit; Yuichi Goto
  Lecture Notes in Artificial Intelligence, Volume：12034, First page：65, Last page：75, Mar. 2020, [Reviewed], [Last]
  Trust reasoning is an indispensable process to establish trustworthy and secure communication under open and decentralized systems that include multi-agents and humans. Trust reasoning is the ability to reason about trust targets and their relationships whether these targets are trusted or not. Reciprocal logics is an expectable candidate for a logic system underlying trust reasoning. However, current reciprocal logics does not cover various trust properties of trust relationship. This paper presents an extends reciprocal logics to deal with various trust properties for trust reasoning. The paper also shows an example of usage the extension logic. The extended logics illustrates the general properties of trust that can facilitate the engineering of trustworthy systems.
  Springer, English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-030-42058-1_6
  DOI ID：10.1007/978-3-030-42058-1_6, ISSN：1611-3349, SCOPUS ID：85082389313
• QSL: A Specification Language for E-Questionnaire, E-Testing, and E-Voting Systems
  Yuan Zhou; Yuichi Goto; Jingde Cheng
  Volume：E102-D, Number：11, First page：2159, Last page：2175, Nov. 2019, [Reviewed], ［International magazine］
  English, Scientific journal
  DOI：https://doi.org/10.1587/transinf.2018EDP7333
  DOI ID：10.1587/transinf.2018EDP7333
• A Supporting Tool for IT System Security Specification Evaluation Based on ISO/IEC 15408 and ISO/IEC 18045
  Da Bao; Yuichi Goto; Jingde Cheng
  Lecture Notes in Computer Science, Volume：11607, First page：3, Last page：14, Sep. 2019, [Reviewed]
  In evaluation and certification framework based on ISO/IEC 15408 and ISO/IEC 18045, a Security Target, which contains the specifications of all security functions of the target system, is the most important document. Evaluation on Security Targets must be performed as the first step of the whole evaluation process. However, evaluation on Security Targets based on ISO/IEC 15408 and ISO/IEC 18045 is very complex. Evaluation process involves of many tasks and costs lots of time when evaluation works are performed by human. Besides, it is also difficult to ensure that evaluation is fair and no subjective mistakes. These issues not only may result in consuming a lot of time, but also may affect the correctness, accuracy, and fairness of evaluation results. Thus, it is necessary to provide a supporting tools that supports all tasks related to the evaluation process automatically to improve the quality of evaluation results at the same time reduce the complexity of all evaluator and certifiers’ work. However, there is no such supporting tool existing until now. This paper proposes a supporting tool, called Security Target Evaluator, that provides comprehensive facilities to support the whole process of evaluation on Security Targets based on ISO/IEC 15408 and ISO/IEC 18045.
  English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-030-26142-9_1
  DOI ID：10.1007/978-3-030-26142-9_1
• Improvement of QSL by Ontologies of E-Questionnaire, E-Testing, and E-Voting Systems　　　　　　　　　　　　　　　
  Yuan Zhou; Yuichi Goto; Jingde Cheng
  Lecture Notes in Electrical Engineering, Volume：590, First page：257, Last page：264, Aug. 2019, [Reviewed]
  QSL is the first specification language for specifying various e-questionnaire, e-testing, and e-voting systems. Although the terminologies among systems and services of e-questionnaire, e-testing, and e-voting are different, QSL has explicitly summed up three kinds of terminologies into one, so that causes QSL has poor usability. The ontologies to summarize the terminologies in e-questionnaire, e-testing, and e-voting systems, to find out the corresponding relations with terminology of QSL, and to clarify the relations of e-questionnaire, e-testing, and e-voting systems can improve usability of QSL, so that the stakeholders can communicate and write requirement specifications easily. However, there is no ontology of e-questionnaire, e-testing, and e-voting systems. This paper proposes the ontologies for e-questionnaire, e-testing, and e-voting systems. Based on the ontologies, we present the improvement of QSL, so that stakeholders can use arbitrary specific terminologies to specify the requirement specifications for other kinds of systems and services.
  English, International conference proceedings
  DOI：https://doi.org/10.1007/978-981-32-9244-4_36
  DOI ID：10.1007/978-981-32-9244-4_36
• An Extension of Formal Analysis Method with Reasoning: A Case Study of Flaw Detection for Non-repudiation and Fairness
  Jingchen Yan; Yating Wang; Yuichi Goto; Jingde Cheng
  Lecture Notes in Computer Science, Volume：11445, First page：399, Last page：408, Apr. 2019, [Reviewed]
  Formal analysis is used to find out flaws of cryptographic protocols. A formal analysis method with reasoning for cryptographic protocols has been proposed. In the method, behaviors of participants and behaviors of an intruder are used as premises of forward reasoning to deduce formulas, then analysts check whether the deduced formulas are related to flaws. However, the method only can detect the flaws related to confidentiality and authentication but is unable to detect the flaws related to non-repudiation and fairness. This paper proposes an extension of the formal analysis method with reasoning, which can deal with the flaws related to non-repudiation and fairness. This paper also shows a case study of flaw detection for non-repudiation and fairness in ISI protocol with the proposed method. The result shows that the proposed method is effective to find out flaws that related to the two security properties above.
  English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-030-16458-4_23
  DOI ID：10.1007/978-3-030-16458-4_23
• An Epistemic Programming Approach for Automated Nonmonotonic Reasoning based on Default Logic
  Yuichi Goto; Takuya Ito
  Proceedings of 2018 IEEE SmartWorld, Ubiquitous Intelligence & Computing, Advanced & Trusted Computing, Scalable Computing & Communications, Cloud & Big Data Computing, Internet of People and Smart City Innovations, First page：222, Last page：227, Oct. 2018, [Reviewed]
  Epistemic programming was proposed as a novel program paradigm to program epistemic processes in scientific discovery, which regards conditionals as the subject of computing, takes primary epistemic operations as basic operations of computing, and regards epistemic processes as the subject of programming. On the other hand, any scientific discovery process may include nonmonotonic reasoning process because knowledge of any scientist is incomplete. However, there is no study about nonmonotonic reasoning under the epistemic programming paradigm. This paper presents an epistemic programming approach for automated nonmonotonic reasoning based on default logic as the first step to achieve automated nonmonotonic reasoning under epistemic programming paradigm.
  English, International conference proceedings
  DOI：https://doi.org/10.1109/SmartWorld.2018.00073
  DOI ID：10.1109/SmartWorld.2018.00073
• A Study on Fine-Grained Security Properties of Cryptographic Protocols for Formal Analysis Method with Reasoning
  Jingchen Yan; Sho Ishibashi; Yuichi Goto; Jingde Cheng
  Proceedings of 2018 IEEE SmartWorld, Ubiquitous Intelligence & Computing, Advanced & Trusted Computing, Scalable Computing & Communications, Cloud & Big Data Computing, Internet of People and Smart City Innovations, First page：210, Last page：215, Oct. 2018, [Reviewed]
  Formal analysis is used to find out flaws of cryptographic protocols. A formal analysis method with reasoning for cryptographic protocols has been proposed. In the method, forward reasoning is used to deduce flaws or situations related to flaws from formalized specifications of cryptographic protocols. Analysts of cryptographic protocols pick up deduced results related to flaws from results of forward reasoning according to some criteria. However, there is no study about the criteria for what are flaws that can be applied to various cryptographic protocols. This paper presents fine-grained security properties that cryptographic protocols should satisfy in order to clarify the criteria. The paper shows the enumerated security properties are correct and valid through analyzing some cryptographic protocols.
  English, International conference proceedings
  DOI：https://doi.org/10.1109/SmartWorld.2018.00071
  DOI ID：10.1109/SmartWorld.2018.00071
• Development of Supporting Environment for IT System Security Evaluation Based on ISO/IEC 15408 and ISO/IEC 18045
  Da Bao; Wen Sun; Yuichi Goto; Jingde Cheng
  Proceedings of 2018 IEEE SmartWorld, Ubiquitous Intelligence & Computing, Advanced & Trusted Computing, Scalable Computing & Communications, Cloud & Big Data Computing, Internet of People and Smart City Innovations, First page：204, Last page：209, Oct. 2018, [Reviewed]
  ISO/IEC 15408 and ISO/IEC 18045 are a pair of international competitive standards for security evaluation and certification of IT systems. Evaluation based on ISO/IEC 15408 and ISO/IEC 18045 is a very complex process that involves tens of documents and tasks. Performing the tasks in evaluation process by human costs a lot of time and it is also difficult to ensure impartial and no subjective mistakes. These issues not only result in consuming a lot of time, but also affect the fairness, correctness and accuracy of evaluation results. A supporting environment was proposed to provide necessary software tools to supports all tasks in the evaluation process automatically to ensure the quality of evaluation resultsat the same time reduce the complexity of all evaluator and certifiers' work. To provide full facilities of the supporting environment, we must clarify every task in the evaluation process and provide appropriate methods for developing supporting tools. This paper deeply analyzes all of the software supportable tasks in the evaluation process and clarifies all detail targets for each task. And then we also provide corresponding methods to support these tasks. This paper also shows a set of developed supporting tools that can perform the evaluation tasks in an organized way.
  English, International conference proceedings
  DOI：https://doi.org/10.1109/SmartWorld.2018.00070
  DOI ID：10.1109/SmartWorld.2018.00070
• Evaluation about the Descriptive Power of QSL: A Specification Language for E-Questionnaire, E-Testing, and E-Voting Systems
  Yuan Zhou; Daisuke Matsuura; Yuichi Goto; Jingde Cheng
  Proceedings of 2018 IEEE SmartWorld, Ubiquitous Intelligence & Computing, Advanced & Trusted Computing, Scalable Computing & Communications, Cloud & Big Data Computing, Internet of People and Smart City Innovations, First page：198, Last page：203, Oct. 2018, [Reviewed]
  QSL is proposed as the first specification language to provide standardized, consistent, and exhaustive specifications for specifying various e-questionnaire, e-testing, and e-voting systems. However, it has not been ascertained whether QSL has enough descriptive power, i.e., whether QSL is enough to specify various e-questionnaire, e-testing, and e-voting systems. This paper presents the evaluation about the descriptive power of QSL manifesting in specifying various e-questionnaire, e-testing, and e-voting systems. As the results, this paper shows that QSL can be used to specify various e-questionnaire, e-testing, and e-voting, as well as the data and the corresponding systems. In addition, QSL is a better tool because the descriptive power of QSL can cover e-questionnaire, e-testing, e-voting, and the corresponding systems.
  English, International conference proceedings
  DOI：https://doi.org/10.1109/SmartWorld.2018.00069
  DOI ID：10.1109/SmartWorld.2018.00069
• Primitive Constituent Elements of Cryptographic Protocols
  Sho Ishibashi; Jingchen Yan; Yuichi Goto; Jingde Cheng
  Proceedings of 2018 IEEE SmartWorld, Ubiquitous Intelligence & Computing, Advanced & Trusted Computing, Scalable Computing & Communications, Cloud & Big Data Computing, Internet of People and Smart City Innovations, First page：192, Last page：197, Oct. 2018, [Reviewed]
  Many cryptographic protocols have been proposed, and many studies of them have been done. However, there is no study to identify constituent elements of cryptographic protocols that are elements of the protocols consist of. The constituent elements can be used for the basis of classification of already proposed cryptographic protocols, the basis of prediction of new cryptographic protocols, and the basis of formal verification for cryptographic protocols. This paper presents primitive constituent element of cryptographic protocols that is an element so that cryptographic protocol cannot accomplish its original tasks without it.
  English, International conference proceedings
  DOI：https://doi.org/10.1109/SmartWorld.2018.00068
  DOI ID：10.1109/SmartWorld.2018.00068
• An Implementation of Theory Grid with Linked Data Technologies
  Tomoya Yamazaki; Atomu Sakuma; Yuichi Goto
  Proceedings of 2018 IEEE SmartWorld, Ubiquitous Intelligence & Computing, Advanced & Trusted Computing, Scalable Computing & Communications, Cloud & Big Data Computing, Internet of People and Smart City Innovations, First page：186, Last page：191, Oct. 2018, [Reviewed]
  The problem of automated theorem finding (ATF problem) is proposed by Wos, and is still one of open problems in automated reasoning. To solve the ATF problem, an ATF method with forward reasoning based on strong relevant logics has been proposed and studied. Theory Grid was proposed as an infrastructure of the ATF method. Theory Grid is a grid computing environment that organizes and manages various formal theories based on various logical systems. Although a data model for the Theory Grid was proposed, there has been no study to construct the Theory Grid yet. This paper presents the first implementation of the Theory Grid. The implementation uses Linked Data technologies to flexibly associate obtained theorems with previously obtained theorems, and to connect a node of the Theory Grid with other nodes of that via Web. By using the Theory Grid, people can easily manage the results of attempts of ATF, and use previously obtained theorems to a next attempt of ATF.
  English, International conference proceedings
  DOI：https://doi.org/10.1109/SmartWorld.2018.00067
  DOI ID：10.1109/SmartWorld.2018.00067
• FreeEnCal Web: a Web Service of Automated Forward Reasoning for General-purpose
  Takumi Otsuka; Kentaro Fukushi; Yuichi Goto; Jingde Cheng
  Proceedings of 2018 IEEE SmartWorld, Ubiquitous Intelligence & Computing, Advanced & Trusted Computing, Scalable Computing & Communications, Cloud & Big Data Computing, Internet of People and Smart City Innovations, First page：180, Last page：185, Oct. 2018, [Reviewed]
  Forward reasoning engine is a computer program to automatically draw new conclusions by repeatedly applying inference rules to given premises and obtained conclusions until some previously specified conditions are satisfied. Although a forward reasoning engine is an indispensable component in various advanced knowledge-based systems with purposes of creation, discovery and prediction, any forward reasoning engine is essentially time-consuming and memory-consuming component. A forward reasoning engine for general purpose, named FreeEnCal, has been proposed and developed, and can be used as a core and fundamental component in the advanced knowledge-based systems. However, it is difficult for users of FreeEnCal to prepare a computational environment that FreeEnCal is running. To solve the problem, this paper presents a Web service for automated forward reasoning, named FreeEnCal Web. Users and programs can use FreeEnCal through Web browsers and Web API without installing FreeEnCal into own computers.
  English, International conference proceedings
  DOI：https://doi.org/10.1109/SmartWorld.2018.00066
  DOI ID：10.1109/SmartWorld.2018.00066
• Improvement of Data Portability of ENQUETE-BAISE: a General-Purpose E-Questionnaire Server for Ubiquitous Questionnaire
  Yohei Kamata; Yuichi Goto
  Proceedings of 2018 IEEE SmartWorld, Ubiquitous Intelligence & Computing, Advanced & Trusted Computing, Scalable Computing & Communications, Cloud & Big Data Computing, Internet of People and Smart City Innovations, First page：174, Last page：179, Oct. 2018, [Reviewed]
  Data portability is the ability for users to reuse their own data between interoperable applications, and is getting treated as an important characteristic of web and cloud services in recent years. Meanwhile, many e-questionnaires are performed on the Internet by some ways of web applications today. ENQUETE-BAISE, a general-purpose e-questionnaire server, is being developed as one of servers that runs e-questionnaires. This paper presents the improvement of data portability of ENQUETE-BAISE. At first, the paper gives the definition of data portability of e-questionnaire systems, and then shows improved ENQUETE-BAISE and the usage. The paper also proposes the advantages of improving the data portability of e-questionnaire systems and the problems caused by improving it.
  English, International conference proceedings
  DOI：https://doi.org/10.1109/SmartWorld.2018.00065
  DOI ID：10.1109/SmartWorld.2018.00065
• A Memory-Efficient Algorithm with Level-Order Unary Degree Sequence for Forward Reasoning Engines
  Hiromu Hiidome; Yuichi Goto; Jingde Cheng
  Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Volume：10751, First page：59, Last page：70, 2018, [Reviewed]
  A forward reasoning engine is an indispensable component in many advanced knowledge-based systems with purposes of creation, discovery, or prediction. Time-efficiency and memory-efficiency are crucial issues for any forward reasoning engine. FreeEnCal is a forward reasoning engine for general-purpose, and has been used for several applications, e.g., automated theorem finding. To improve time-efficiency, current implementation of FreeEnCal uses “trie”, which is a kind of tree structure, to store all logical formulas that are given or deduced in FreeEnCal. However, the implementation is not so memory-efficient from view point of applications of FreeEnCal. The paper presents a memory-efficient algorithm of FreeEnCal, and shows theoretical evaluation of the algorithm. The algorithm uses level-order unary degree sequence (LOUDS) that is a kind of succinct data structures and is used to represent tree structures concisely. By using LOUDS to construct trie in FreeEnCal, we can improve memory-efficiency of FreeEnCal.
  Springer Verlag, English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-319-75417-8_6
  DOI ID：10.1007/978-3-319-75417-8_6, ISSN：1611-3349, ORCID：42008666, SCOPUS ID：85043538369
• A Predicate Suggestion Algorithm for Automated Theorem Finding with Forward Reasoning　　　　　　　　　　　　　　　
  Yuichi Goto; Hongbiao Gao; Jingde Cheng
  INTELLIGENT INFORMATION AND DATABASE SYSTEMS (ACIIDS 2017), PT II, Volume：10192, First page：125, Last page：134, 2017, [Reviewed]
  The problem of automated theorem finding (ATF for short) is one of the 33 basic research problems in automated reasoning. To solve the ATF problem, an ATF method with forward reasoning based on strong relevant logics has been proposed and studied. In the method, predicate abstraction plays important role. However, in the current method, targets of predicate abstraction are predicates that an executor of ATF has already known. This paper presents a predicate suggestion algorithm to suggest previously unknown predicates and create abstraction rules for predicate abstraction in the ATF method with forward reasoning. The paper also shows that the proposed algorithm is effective through a case study.
  SPRINGER INT PUBLISHING AG, English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-319-54430-4_13
  DOI ID：10.1007/978-3-319-54430-4_13, ISSN：0302-9743, ORCID：38326583, SCOPUS ID：85018470490, Web of Science ID：WOS:000401653300013
• A Supporting Tool for Spiral Model of Cryptographic Protocol Design with Reasoning-Based Formal Analysis　　　　　　　　　　　　　　　
  Kazunori Wagatsuma; Tsubasa Harada; Shogo Anze; Yuichi Goto; Jingde Cheng
  ADVANCED MULTIMEDIA AND UBIQUITOUS ENGINEERING: FUTURE INFORMATION TECHNOLOGY, VOL 2, Volume：354, First page：25, Last page：32, 2016, [Reviewed]
  Many cryptographic protocols proposed to securely send and receive information with someone in unsecured network for various purposes. To design secure cryptographic protocols, formal analysis for cryptographic protocols should be included as an essential activity in a process of cryptographic protocol design. In other word, the ideal process consists of design, formalization, formal analysis, interpretation, and improvement, and the five activities are done repeatedly as similar as activities in spiral model of software development. This paper presents a supporting tool for the ideal process of cryptographic protocol design. At first, the paper presents the spiral model of cryptographic protocol design, and introduces formal analysis method with reasoning as a suitable formal analysis method for the spiral model. The paper also presents design of the supporting tool and its implementation for key exchange protocols. By the supporting tool, designers can only focus on design and improvement activities in the spiral model.
  SPRINGER, English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-662-47895-0_4
  DOI ID：10.1007/978-3-662-47895-0_4, ISSN：1876-1100, ORCID：38326582, SCOPUS ID：84947237884, Web of Science ID：WOS:000381756300004
• Predicting new attacks for information security
  Da Bao; Yuichi Goto; Jingde Cheng
  Lecture Notes in Electrical Engineering, Volume：330, First page：1353, Last page：1358, 2015, [Reviewed]
  Our knowledge base of attacks is always not enough for developing and maintaining information systems. An information system, which is developed and maintained according to an insufficient knowledge base of attacks, has no capability of defending against new attacks from the complicated environment. To mitigate this circumstance, we should continuously predict new attacks and add them into the knowledge base of attacks such that by enriching the knowledge base of attacks, information systems can be developed and maintained more countermeasures to confront those new attacks. However, there is no methodology proposed for predicting new attacks. This paper presents an analysis and discussion for predicting new attacks and shows the challenges issues in predicting new attacks. The paper also proposes a reasoning method for predicting new threats.
  Springer Verlag, English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-662-45402-2_188
  DOI ID：10.1007/978-3-662-45402-2_188, ISSN：1876-1119, ORCID：38326585, SCOPUS ID：84915747262
• Explicitly Epistemic Contraction by Predicate Abstraction in Automated Theorem Finding: A Case Study in NBG Set Theory　　　　　　　　　　　　　　　
  Hongbiao Gao; Yuichi Goto; Jingde Cheng
  Intelligent Information and Database Systems, Pt I, Volume：9011, First page：593, Last page：602, 2015, [Reviewed]
  In automated theorem finding by forward reasoning, there are many redundant theorems as intermediate results. This paper proposes an approach of explicitly epistemic contraction by predicate abstraction for automated theorem finding by forward reasoning in order to remove redundant theorems in a set of obtained theorems, and shows the effectiveness of the explicitly epistemic contraction by a case study of automated theorem finding in NBG set theory.
  SPRINGER INT PUBLISHING AG, English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-319-15702-3_57
  DOI ID：10.1007/978-3-319-15702-3_57, ISSN：0302-9743, ORCID：38326596, SCOPUS ID：84925260368, Web of Science ID：WOS:000389499200057
• Development of a Bidirectional Transformation Supporting Tool for Formalization with Logical Formulas and Its Application　　　　　　　　　　　　　　　
  Shunsuke Nanaumi; Kazunori Wagatsuma; Hongbiao Gao; Yuichi Goto; Jingde Cheng
  Advanced Multimedia and Ubiquitous Engineering: Future Information Technology, Volume：352, First page：1, Last page：6, 2015, [Reviewed]
  In many applications in computer science and artificial intelligence, logical formulas are used as a formal representation to represent and/or specify various objects and relationships among them. Transforming logical formulas into informal propositional statements, e.g., declarative sentences and mathematical formulas, is important as well as transforming informal propositional statements into logical formulas. When people obtain new logical formulas as results of deduction/reasoning based on logic, investigating the obtained formulas is also not an easy task for them. Although information systems with proving, e.g., automated theorem proving systems, formal verification systems, etc., are used in various field, in the future, information systems with reasoning, e.g., automated theorem finding systems, will also be developed and used in various fields. Thus, a tool to support bidirectional transformation between informal propositional statements and logical formulas will be demanded at that time. This paper presents an implementation of a bidirectional transformation supporting tool for formalization with logical formulas. The paper also shows application of the tool in a case study of automated theorem finding with forward reasoning.
  SPRINGER, English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-662-47487-7_1
  DOI ID：10.1007/978-3-662-47487-7_1, ISSN：1876-1100, ORCID：38326590, SCOPUS ID：84937436367, Web of Science ID：WOS:000380566900001
• Development of ISMEE: An information security management engineering environment
  Ahmad Iqbal Hakim Suhaimi; Da Bao; Yuichi Goto; Jingde Cheng
  Lecture Notes in Electrical Engineering, Volume：330, First page：1325, Last page：1330, 2015, [Reviewed]
  An Information Security Management System (ISMS) has become more important for any organization to manage its information assets securely. However, it is not easy for the organization to establish own ISMS, and for employees to work according to the ISMS. Therefore, ISMEE, an Information Security Management Engineering Environment, was proposed as the first engineering environment for supporting organizations with ISMSs. ISMEE integrates various tools to support all participants in an organization to perform all tasks in from preparation to abolishment of an ISMS based on ISO/IEC 27000 series, which are the international standards for ISMSs. This paper presents our implementation of ISMEE. At first, the paper investigates technical issues to realize ISMEE. Then, the paper shows how the issues are addressed and presents our current implementation of ISMEE.
  Springer Verlag, English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-662-45402-2_184
  DOI ID：10.1007/978-3-662-45402-2_184, ISSN：1876-1119, ORCID：38326579, SCOPUS ID：84915820190
• Automated Theorem Finding by Forward Reasoning Based on Strong Relevant Logic: A Case Study in Graph Theory　　　　　　　　　　　　　　　
  Hongbiao Gao; Yuichi Goto; Jingde Cheng
  Advanced Multimedia and Ubiquitous Engineering: Future Information Technology, Volume：352, First page：23, Last page：30, 2015, [Reviewed]
  The problem of automated theorem finding is one of 33 basic research problems in automated reasoning which was originally proposed by Wos. The problem is still an open problem until now. To solve the problem, a systematic methodology with forward reasoning based on strong relevant logic has been proposed. This paper presents a case study of automated theorem finding in graph theory to show the generality of the methodology, and presents a future direction for automated theorem finding based on the methodology.
  SPRINGER, English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-662-47487-7_4
  DOI ID：10.1007/978-3-662-47487-7_4, ISSN：1876-1100, ORCID：38326587, SCOPUS ID：84937424485, Web of Science ID：WOS:000380566900004
• An Extension of QSL for E-testing and Its Application in an Offline E-testing Environment　　　　　　　　　　　　　　　
  Zhe Wang; Yuan Zhou; Bo Wang; Yuichi Goto; Jingde Cheng
  Advanced Multimedia and Ubiquitous Engineering: Future Information Technology, Volume：352, First page：7, Last page：14, 2015, [Reviewed]
  E-testing is to perform all processes from preparing questions to marking collected answer of the questions in a completely electronic way. Now, various e-testing are done, and there are many kinds of e-testing systems. When people want to do an e-testing or order a new e-testing system, they should specify the e-testing or e-testing system. A Specification language helps to create precise and adequate specifications of e-testing and e-testing systems is demanded. QSL is a specification language for specifying various e-questionnaire and e-questionnaire systems. QSL is a hopeful candidate of the required specification language because both testing and questionnaire have similar processes. However, the current version of QSL does not take e-testing and e-testing systems into account. This paper presents an extension of QSL to deal with e-testing and e-testing systems, and shows a real application of extended QSL in case of an offline e-testing environment.
  SPRINGER, English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-662-47487-7_2
  DOI ID：10.1007/978-3-662-47487-7_2, ISSN：1876-1100, ORCID：38326591, SCOPUS ID：84937427178, Web of Science ID：WOS:000380566900002
• A Tasking Deadlock Detector for Ada 2012 Programs　　　　　　　　　　　　　　　
  Bo Wang; Takeo Ekiba; Yuichi Goto; Jingde Cheng
  Advanced Multimedia and Ubiquitous Engineering: Future Information Technology, Volume：352, First page：15, Last page：22, 2015, [Reviewed]
  To avoid and resolve tasking deadlocks in Ada programs, it is indispensable to identify and detect all types of tasking deadlocks. Various combinations of synchronization waiting relations concerning synchronization waiting tasks may lead to various types of tasking deadlocks. As a substantial expansion of Ada 2005, Ada 2012 has many new facilities, and therefore, these changes have a great impact on Ada tasking deadlocks and their detection. Though a tasking deadlock detector for Ada 2005 and Ada 95 was developed, it cannot detect new types of tasking deadlocks in Ada 2012 programs. This paper presents a new tasking deadlock detector for Ada 2012 programs that we are developing. At first, we analyzed various types of tasking deadlocks concerning new synchronization waiting relations defined in Ada 2012. After that we designed the tasking deadlock detector, and implemented it.
  SPRINGER, English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-662-47487-7_3
  DOI ID：10.1007/978-3-662-47487-7_3, ISSN：1876-1100, ORCID：38326586, SCOPUS ID：84937397638, Web of Science ID：WOS:000380566900003
• A supporting environment for IT system security evaluation based on ISO/IEC 15408 and ISO/IEC 18045
  Huilin Chen; Da Bao; Yuichi Goto; Jingde Cheng
  Lecture Notes in Electrical Engineering, Volume：330, First page：1359, Last page：1366, 2015, [Reviewed]
  ISO/IEC 15408 and ISO/IEC 18045 are a pair of international standards for security evaluation and certification of IT systems. However, security evaluation based on this pair of standards is not an easy work. There are many activities and documents in the whole evaluation process. Complicated tasks in evaluation process may cause people making mistakes in intermediate products and evaluation results. It is also difficult to ensure that evaluation is fair and transparent, although each evaluator tries to evaluate a target system earnestly, evaluation results may be different because of evaluators' biases. Moreover, to manage a lot of intermediate products in evaluation process is not easy task even for experienced evaluators. This paper presents a supporting environment for IT system security evaluation based on ISO/IEC 15408 and ISO/IEC 18045 which can support all tasks related to security evaluation by guiding and helping evaluators to perform these tasks regularly, and also can support the management of all documents and intermediate products in the whole evaluation process.
  Springer Verlag, English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-662-45402-2_189
  DOI ID：10.1007/978-3-662-45402-2_189, ISSN：1876-1119, ORCID：38326584, SCOPUS ID：84915822474
• A Set of Metrics for Measuring Interestingness of Theorems in Automated Theorem Finding by Forward Reasoning: A Case Study in NBG Set Theory　　　　　　　　　　　　　　　
  Hongbiao Gao; Yuichi Goto; Jingde Cheng
  INTELLIGENCE SCIENCE AND BIG DATA ENGINEERING: BIG DATA AND MACHINE LEARNING TECHNIQUES, ISCIDE 2015, PT II, Volume：9243, First page：508, Last page：517, 2015, [Reviewed]
  The problem of automated theorem finding is one of 33 basic research problems in automated reasoning which was originally proposed by Wos in 1988, and it is still an open problem. The problem implicitly requires some metrics to be used for measuring interestingness of found theorems. However, no one addresses that requirement until now. This paper proposes the first set of metrics for measuring interestingness of theorems. The paper also presents a case study in NBG set theory, in which we use the proposed metrics to measure the interestingness of the theorems of NBG set theory obtained by using forward reasoning approach and confirms the effectiveness of the metrics.
  SPRINGER INT PUBLISHING AG, English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-319-23862-3_50
  DOI ID：10.1007/978-3-319-23862-3_50, ISSN：0302-9743, ORCID：38326588, SCOPUS ID：84945957469, Web of Science ID：WOS:000374477000050
• A Bidirectional Transformation Supporting Tool for Formalization with Logical Formulas　　　　　　　　　　　　　　　
  Shunsuke Nanaumi; Kazunori Wagatsuma; Hongbiao Gao; Yuichi Goto; Jingde Cheng
  Intelligent Information and Database Systems, Pt I, Volume：9011, First page：634, Last page：643, 2015, [Reviewed]
  In many applications in computer science and artificial intelligence, logical formulas are used as a formal representation to represent and/or specify various objects and relationships among them. However, transforming the informal propositional statements, e.g., declarative sentences and mathematical formulas, into logical formulas is not an easy task for most people. Moreover, when people obtain new logical formulas as results of deduction/reasoning based on logic, investigating the obtained formulas is also not an easy task for them. Although a tool to support transformation from the informal propositional statements of a target domain into logical formulas, and vice versa, is demanded, there is no such tool until now. This paper presents a bidirectional transformation method for formalization with logical formulas, and its supporting tool we are developing.
  SPRINGER INT PUBLISHING AG, English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-319-15702-3_61
  DOI ID：10.1007/978-3-319-15702-3_61, ISSN：0302-9743, ORCID：38326592, SCOPUS ID：84925274566, Web of Science ID：WOS:000389499200061
• Aspect-oriented reuse mechanism for security targets and protection profiles　　　　　　　　　　　　　　　
  Yuichi Goto; Huilin Chen; Da Bao
  Proceedings of the IEEE International Conference on Software Engineering and Service Sciences, ICSESS, First page：161, Last page：164, Oct. 2014, [Reviewed]
  Common Criteria (CC) is an international standard for evaluation and certification of IT products. Although a security target (ST) is an important and central document used in the security evaluation process of CC, creating STs is not so easy task for most of software engineers. On the other hand, there are dependency relations among several elements of an ST and a protection profile (PP). Elements of an ST/PP are elements of mandatory contents of STs/PPs defined in CC part 1, e.g., security problems, security objectives, security requirements, and so on. If there is a same element in both an ST/PP and other ST/PP, then what to describe and how to describe elements that depend on the same element are probably similar. Such same element and its dependent elements are a cross-cutting concern among the STs/PPs. Although retrieving cross-cutting concerns among certified STs and PPs are useful for creation and evaluation of STs and PPs, it is difficult, not impossible, to do that because certified STs and PPs are published as PDF files. This paper presents an aspect-oriented reuse mechanism for STs and PPs to help creation and evaluation of STs. The paper also shows technical issues and current implementation of the mechanism.
  IEEE Computer Society, English, International conference proceedings
  DOI：https://doi.org/10.1109/ICSESS.2014.6933536
  DOI ID：10.1109/ICSESS.2014.6933536, ISSN：2327-0594, SCOPUS ID：84910042594
• A systematic methodology for automated theorem finding　　　　　　　　　　　　　　　
  Hongbiao Gao; Yuichi Goto; Jingde Cheng
  THEORETICAL COMPUTER SCIENCE, Volume：554, Number：C, First page：2, Last page：21, Oct. 2014, [Reviewed]
  The problem of automated theorem finding is one of the 33 basic research problems in automated reasoning which was originally proposed by Wos in 1988, and it is still an open problem. To solve the problem, an approach of forward deduction based on the strong relevant logics was proposed. Following the approach, this paper presents a systematic methodology for automated theorem finding. To show the effectiveness of our methodology, the paper presents two case studies, one is automated theorem finding in NBG set theory and the other is automated theorem finding in Peano's arithmetic. Some known theorems have been found in our case studies. (C) 2014 Elsevier B.V. All rights reserved.
  ELSEVIER SCIENCE BV, English, Scientific journal
  DOI：https://doi.org/10.1016/j.tcs.2014.06.028
  DOI ID：10.1016/j.tcs.2014.06.028, ISSN：0304-3975, eISSN：1879-2294, ORCID：38326594, SCOPUS ID：84925246258, Web of Science ID：WOS:000343639100002
• An Information Security Management Database System (ISMDS) for Engineering Environment Supporting Organizations with ISMSs　　　　　　　　　　　　　　　
  Ahmad Iqbal Hakim Suhaimi; Yuichi Goto; Jingde Cheng
  IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, Volume：E97D, Number：6, First page：1516, Last page：1527, Jun. 2014, [Reviewed]
  Information Security Management Systems (ISMSs) play important roles in helping organizations to manage their information securely. However, establishing, managing, and maintaining ISMSs is not an easy task for most organizations because an ISMS has many participants and tasks, and requires many kinds Of documents. Therefore, organizations with ISMSs demand tools that can support them to perform all tasks in ISMS lifecycle processes consistently and continuously. To realize such support tools, a database system that manages ISO/EEC 27000 series, which are international standards for ISMSs, and ISMS documents, which are the products of tasks in ISMS lifecycle processes, is indispensable. The database system should manage data of the standards and documents for all available versions and translations, relationship among the standards and documents, authorization to access the standards and documents, and metadata of the standards and documents. No such database system has existed until now. This paper presents an information security management database system (ISMDS) that manages ISO/EEC 27000 series and ISMS documents. ISMDS is a meta-database system that manages several databases of standards and documents. ISMDS is used by participants in ISMS as well as tools supporting the participants to perform tasks in ISMS lifecycle processes. The users or tools can retrieve data from all versions and translations of the standards and documents. The paper also presents some use cases to show the effectiveness of ISMDS.
  IEICE-INST ELECTRONICS INFORMATION COMMUNICATIONS ENG, English, Scientific journal
  DOI：https://doi.org/10.1587/transinf.E97.D.1516
  DOI ID：10.1587/transinf.E97.D.1516, ISSN：1745-1361, ORCID：14254531, SCOPUS ID：84901798149, Web of Science ID：WOS:000342784300014
• QSL: A Specification Language for E-questionnaire Systems　　　　　　　　　　　　　　　
  Yuan Zhou; Yuichi Goto; Jingde Cheng
  2014 5TH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND SERVICE SCIENCE (ICSESS), First page：224, Last page：230, 2014, [Reviewed]
  Questionnaire is a general and indispensable method used frequently and widely in many academic, engineering, medical, commercial and political survey research activities to collect information about opinion or behavior of some groups of people. Today, many questionnaires are performed on the Internet by some ways of web applications. However, until now, there is no questionnaire specification language that can be used to specify various e-questionnaire systems. This paper proposes the first specification language named "QSL" for various e-questionnaire systems. QSL can be used to specify not only various questionnaires but also various e-questionnaire systems. The paper presents an analysis of the primitive elements of questionnaires and e-questionnaire systems, defines the specification language QSL, and discusses its completeness and effectiveness.
  IEEE, English, International conference proceedings
  Web of Science ID：WOS:000355926400049
• User management in Information Security Engineering Environment ISEE
  Yuichi Goto; Liqing Xu; Ning Zhang; Jingde Cheng
  Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Volume：8440, First page：18, Last page：34, 2014, [Reviewed]
  An Information Security Engineering Environment (ISEE) based on ISO/IEC security standards has been proposed. ISEE integrates various tools such that its users can use these tools to ensure the whole security of their target information system at anytime consistently and continuously according to ISO/IEC security standards. In order to defend attacks and prevent damage beforehand, ISEE should provide users with some way to control user behavior by giving appropriate suggestions anticipatorily and actively. Such facility to control user behavior should be provided by a user management mechanism of ISEE, i.e., the user management mechanism of ISEE should deal with not only authentication, authorization, accounting or auditing, but also generating effective suggestions from records of user behavior anticipatorily, and informing the suggestions actively. Any traditional user management system is a storehouse of user data and works passively according to queries or transactions explicitly issued by its users and/or application programs, but has no active behavior to do something by itself. This paper presents an anticipatory user management mechanism of ISEE, as a new type of user management mechanism for SaaS-based cloud services with facility to control user behavior. © 2014 Springer International Publishing.
  Springer Verlag, English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-319-06677-6_3
  DOI ID：10.1007/978-3-319-06677-6_3, ISSN：1611-3349, ORCID：14254530, SCOPUS ID：84901684450
• Strong relevant logic-based reasoning as an information mining method in big information era
  Yuichi Goto
  Lecture Notes in Electrical Engineering, Volume：309, First page：9, Last page：16, 2014, [Reviewed]
  Dealing with Big Data is one of the emerging issues in our society. After a decade or two decades from now, it will become one of operations in our everyday works. What is a new issue at that time? It will be dealing with Big Information. This paper investigates information mining for Big Information as a new challenging issue. The paper also shows that strong relevant logic-based reasoning is one of systematic methods for the information mining, and discusses the automation of information mining with strong relevant logic-based reasoning. © 2014 Springer-Verlag Berlin Heidelberg.
  Springer Verlag, English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-642-55038-6_2
  DOI ID：10.1007/978-3-642-55038-6_2, ISSN：1876-1119, ORCID：14254533, SCOPUS ID：84902358528
• Research on automated theorem finding: Current state and future directions
  Hongbiao Gao; Yuichi Goto; Jingde Cheng
  Lecture Notes in Electrical Engineering, Volume：309, First page：105, Last page：110, 2014, [Reviewed]
  The problem of automated theorem finding is one of 33 basic research problems in automated reasoning which was originally proposed by Wos. The problem is still an open problem until now. This paper reviews the current state of the research on automated theorem finding and shows some future directions of automated theorem finding. In particular, we propose a systematic procedure for automated theorem finding based on Cheng's approach, i.e., automated theorem finding by forward deduction based on strong relevant logics. © 2014 Springer-Verlag Berlin Heidelberg.
  Springer Verlag, English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-642-55038-6_16
  DOI ID：10.1007/978-3-642-55038-6_16, ISSN：1876-1119, ORCID：14254532, SCOPUS ID：84902383982
• Formalization for formal analysis of cryptographic protocols with reasoning approach
  Kazunori Wagatsuma; Shogo Anze; Yuichi Goto; Jingde Cheng
  Lecture Notes in Electrical Engineering, Volume：309, First page：211, Last page：218, 2014, [Reviewed]
  Formal analysis of cryptographic protocols is necessary to find flaws before using them. However, in traditional approaches based on proving, it is difficult for analysts to enumerate all security goals for proving that a cryptographic protocol is secure because analysts sometimes overlook or do not recognize some security goals. Reasoning approach was proposed as an alternative approach, but its concrete method has not been established yet. In order to establish the concrete method, this paper presents a method of formalization for formal analysis of cryptographic protocols with reasoning approach. The paper presents a method of formalization for key exchange protocols, shows that it can be applied to any key exchange protocols, and shows that it can be extended to be applied to various cryptographic protocols. © 2014 Springer-Verlag Berlin Heidelberg.
  Springer Verlag, English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-642-55038-6_32
  DOI ID：10.1007/978-3-642-55038-6_32, ISSN：1876-1119, ORCID：14254535, SCOPUS ID：84902370160
• An engineering environment based on ISO/IEC 27000 series standards for supporting organizations with ISMSs
  Ahmad Iqbal Hakim Suhaimi; Yuichi Goto; Jingde Cheng
  Lecture Notes in Electrical Engineering, Volume：309, First page：195, Last page：201, 2014, [Reviewed]
  Information Security Management Systems (ISMSs) play important roles to manage organization's information assets securely. However, organizations with ISMSs facing various challenges to develop and maintain such a complex management system effectively. Such organizations demand tools that can provide them with comprehensive support for all tasks in ISMS. This paper presents an engineering environment to support organizations with ISMSs consistently and continuously based on ISO/IEC 27000 series. At first, the paper presents challenges in ISMS and requirements analysis to address the challenges. The paper, then, presents an architecture and some use cases of the environment. © 2014 Springer-Verlag Berlin Heidelberg.
  Springer Verlag, English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-642-55038-6_30
  DOI ID：10.1007/978-3-642-55038-6_30, ISSN：1876-1119, ORCID：14254534, SCOPUS ID：84902367860
• Active and personalized services in an information security engineering cloud based on ISO/IEC 15408
  Liqing Xu; Yuichi Goto; Ahmad Iqbal Hakim Suhaimi; Ning Zhang; Jingde Cheng
  Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Volume：8440, First page：35, Last page：48, 2014, [Reviewed]
  An Information Security Engineering Environment (ISEE) based on ISO/IEC security standards has been proposed. It integrates various tools such that its users can use these tools to ensure the whole security of their target information system at anytime consistently and continuously according to ISO/IEC security standards. But ISEE can only provide its services passively, i.e., when users use ISEE, they have to give some commands or instructions to ISEE. Because crackers are active persons who can get knowledge and skills day after day and then continuously attack the weakest point or connection in each target system always with new techniques, some active services and personalized services to defend attacks and prevent damage beforehand are very desirable to various users of ISEE. We have proposed an Information Security Engineering Cloud (ISEC) as a platform to provide various active services and personalized services based on ISEE to its various users in a way of cloud services. ISO/IEC 15408, as one of the most important international standards, plays an important role to ensure the whole security of target information/software systems, and therefore, has been adopted as the core standard in ISEC. This paper presents a control mechanism to provide active and personalized serviced based on ISO/IEC 15408. In order to realize this mechanism, we defined active and personalized services of ISEC, and analyzed necessary data of checkpoints, which are the items controlled by a series of tasks for managing task progress based on ISO/IEC 15408. Based on the analysis, we show how to provide active and personalized services to meet the different needs of various users. © 2014 Springer International Publishing.
  Springer Verlag, English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-319-06677-6_4
  DOI ID：10.1007/978-3-319-06677-6_4, ISSN：1611-3349, ORCID：14254536, SCOPUS ID：84901684852
• Anticipatory Runway Incursion Prevention Systems　　　　　　　　　　　　　　　
  Kai Shi; Yuichi Goto; Zhiliang Zhu; Jingde Cheng
  IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, Volume：E96D, Number：11, First page：2385, Last page：2396, Nov. 2013, [Reviewed]
  Avoiding runway incursions is a significant challenge and a top priority in aviation. Due to all causes of runway incursions belong to human factors, runway incursion prevention systems should remove human from the system operation loop as much as possible. Although current runway incursion prevention systems have made big progress on how to obtain accurate and sufficient information of aircraft/vehicles, they cannot predict and detect runway incursions as early as experienced air traffic controllers by using the same surveillance information, and cannot give explicit instructions and/or suggestions to prevent runway incursions like real air traffic controllers either. In one word, human still plays an important position in current runway incursion prevention systems. In order to remove human factors from the system operation loop as much as possible, this paper proposes a new type of runway incursion prevention system based on logic-based reasoning. The system predicts and detects runway incursions, then gives explicit instructions and/or suggestions to pilots/drivers to avoid runway incursions/collisions. The features of the system include long-range prediction of incidents, explicit instructions and/or suggestions, and flexible model for different policies and airports. To evaluate our system, we built a simulation system, and evaluated our system using both real historical scenarios and conventional fictional scenarios. The evaluation showed that our system is effective at providing earlier prediction of incidents than current systems, giving explicit instructions and/or suggestions for handling the incidents effectively, and customizing for specific policies and airports using flexible model.
  IEICE-INST ELECTRONICS INFORMATION COMMUNICATIONS ENG, English, Scientific journal
  DOI：https://doi.org/10.1587/transinf.E96.D.2385
  DOI ID：10.1587/transinf.E96.D.2385, ISSN：0916-8532, eISSN：1745-1361, Web of Science ID：WOS:000327168600009
• Supporting Verification and Validation of Security Targets with ISO/IEC 15408　　　　　　　　　　　　　　　
  Da Bao; Junichi Miura; Ning Zhang; Yuichi Goto; Jingde Cheng
  PROCEEDINGS 2013 INTERNATIONAL CONFERENCE ON MECHATRONIC SCIENCES, ELECTRIC ENGINEERING AND COMPUTER (MEC), First page：2621, Last page：2628, 2013, [Reviewed]
  ISO/IEC 15408 is an international standard for security evaluation of information systems, and can be applied throughout the software life cycle to improve security of information systems. A Security Target, which contains specifications of security functions of the target system, is the most important document in development of the system according to ISO/IEC 15408. Verification and Validation of Security Targets must be strictly performed before development of the system. This paper analyzed and clarified 168 targets that Security Targets must satisfy based on ISO/IEC 18045, and the procedures of examining those targets are also provided. Then the paper proposes comprehensive methods to support verification and validation of Security Targets. With these methods, we can implement comprehensive supporting tools for verification and validation of Security Targets.
  IEEE, English, International conference proceedings
  Web of Science ID：WOS:000366663002019
• Supporting Tools for Software Supportable Tasks Related with ISO/IEC 15408　　　　　　　　　　　　　　　
  Ning Zhang; Da Bao; Liqing Xu; A. I. H. Suhaimi; Junichi Miura; Yuichi Goto; Jingde Cheng
  PROCEEDINGS 2013 INTERNATIONAL CONFERENCE ON MECHATRONIC SCIENCES, ELECTRIC ENGINEERING AND COMPUTER (MEC), First page：2002, Last page：2006, 2013, [Reviewed]
  ISO/IEC 15408, one of international security standards, plays an important role to ensure whole security of information/software systems. Software supportable tasks related with ISO/IEC 15408 have been analyzed as a basic to construct an information security engineering environment (ISEE). However, it does not clarify what kinds of supporting tools are necessary for those software supportable tasks. In order to provide practical support, it is necessary to provide various supporting tools for the tasks. This paper analyzes deeply the software supportable tasks related with ISO/IEC 15408, analyzed requirements of supporting tools, and proposes a series of supporting tools for the tasks as the core of ISEE. These tools can be integrated to provide comprehensives facilities to perform the tasks consistently and continuously related with ISO/IEC 15408.
  IEEE, English, International conference proceedings
  Web of Science ID：WOS:000366663001136
• Making existing reactive systems anticipatory
  Kai Shi; Yuichi Goto; Zhiliang Zhu; Jingde Cheng
  Studies in Computational Intelligence, Volume：493, First page：17, Last page：32, 2013, [Reviewed]
  From the viewpoints of high safety and high security, any critical reactive system should be anticipatory, i.e., the system should be able to detect and predict accidents/attacks, take some actions to inform its users, and perform some operations to defend the system from possible accidents/attacks anticipatorily.However, most of existing reactive systems are not so, furthermore, it is impractical, but not impossible, to rebuild them to be anticipatory, because reimplementation of the whole of a system results in high cost. Therefore, it is desirable to extend an existing legacy reactive system with anticipatory ability without reimplementing the whole of the legacy system. This paper proposes a general methodology to realize such an extension. The novelty of the methodology is that it does not require reimplementation the whole legacy system, does not affect the system's original functions, and can deal with various reactive systems by using the same process. By extending an existing reactive system anticipatory using our methodology, we can get a new generation system with high safety and high security. This paper also presents three case studies to show how to apply our methodology. © Springer International Publishing Switzerland 2013.
  Springer Verlag, English, Scientific journal
  DOI：https://doi.org/10.1007/978-3-319-00804-2_2
  DOI ID：10.1007/978-3-319-00804-2_2, ISSN：1860-949X, ORCID：10636970, SCOPUS ID：84884990490
• Finding theorems in NBG set theory by automated forward deduction based on strong relevant logic
  Hongbiao Gao; Kai Shi; Yuichi Goto; Jingde Cheng
  Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Volume：7936, First page：697, Last page：704, 2013, [Reviewed]
  Automated theorem finding is one of 33 basic research problems in automated reasoning which was originally proposed by Wos in 1988, and it is still an open problem. For the problem, Cheng has proposed a forward deduction approach based on strong relevant logic. To verify the effectiveness of the approach, we tried to rediscover already known theorems in NBG set theory by using the approach, and succeeded in rediscovery of several known theorems. However, the method of the rediscovery is ad hoc, but not systematic. This paper gives an analysis and discussion for our experiment method and results from the viewpoint of the systematic method. The paper also presents some issues and future research directions for a systematic method of automated theorem finding based on Cheng's approach. © 2013 Springer-Verlag Berlin Heidelberg.
  English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-642-38768-5_62
  DOI ID：10.1007/978-3-642-38768-5_62, ISSN：0302-9743, ORCID：10636971, SCOPUS ID：84884957061
• DEVELOPMENT OF A SUPPORTING TOOL FOR TRANSLATION BETWEEN DECLARATIVE SENTENCES AND LOGICAL FORMULAS　　　　　　　　　　　　　　　
  Shunsuke Nanaumi; Kazunori Wagatsuma; Yuichi Goto; Jingde Cheng
  PROCEEDINGS OF 2013 INTERNATIONAL CONFERENCE ON MACHINE LEARNING AND CYBERNETICS (ICMLC), VOLS 1-4, Volume：3, First page：1179, Last page：1184, 2013, [Reviewed]
  Logical formulas are often used as a representation form to describe knowledge in many intelligent system applications. However, it is not an easy task to translate declarative sentences into logical formulas. On the other hand, in some intelligent system applications, it is necessary to translate logical formulas into declarative sentences for usual. To do the translation, the correspondence between the vocabulary of the logical formulas and that of declarative sentences is demanded. Thus, a supporting tool for translation from logical formulas to declarative sentences must cooperate with a supporting tool for translation from declarative sentences to logical formulas. However, there are no reports about such supporting tools.
  This paper presents a supporting tool for translation between declarative sentences and logical formulas. The tool works with its users in an interactive mode. The tool makes users revise a target declarative sentence in order to translate declarative sentences into logical formulas. It also translates revised declarative sentences into logical formulas according to its user's instructions, and records correspondence between the vocabulary of declarative sentences and that of logical formulas. Moreover, it translates logical formulas into declarative sentences according to the correspondence. By using our supporting tool, one can easily translate the declarative sentences into logical formulas, and vice versa.
  IEEE, English, International conference proceedings
  DOI：https://doi.org/10.1109/ICMLC.2013.6890769
  DOI ID：10.1109/ICMLC.2013.6890769, ISSN：2160-133X, ORCID：14254541, SCOPUS ID：84907270680, Web of Science ID：WOS:000366853800162
• Automated theorem finding by forward deduction based on the semi-lattice model of formal theory: A case study in nbg set theory
  Hongbiao Gao; Yuichi Goto; Jingde Cheng
  Proceedings - 2013 9th International Conference on Semantics, Knowledge and Grids, SKG 2013, First page：22, Last page：29, 2013, [Reviewed]
  The problem of automated theorem finding is one of 33 basic research problems in automated reasoning which was originally proposed by Wos in 1988, and it is still an open problem. To solve the problem, a forward deduction approach based on the strong relevant logics was proposed. To verify the effectiveness of the approach, we tried to rediscover already known theorems in NBG set theory by using the approach, and succeeded in rediscovery of several known theorems. However, from the viewpoint of automated theorem finding, our method of the rediscovery is ad hoc, but not systematic. This paper proposes a systematic method based on the semi-lattice model of formal theory for deducing theorems and finding theorems which are two key phases of automated theorem finding. The paper presents a case study for automated theorem finding in NBG set theory and also shows some future research directions for automated theorem finding. © 2013 IEEE.
  IEEE Computer Society, English, International conference proceedings
  DOI：https://doi.org/10.1109/SKG.2013.36
  DOI ID：10.1109/SKG.2013.36, ORCID：14254542, SCOPUS ID：84902162663
• Anticipatory Emergency Elevator Evacuation Systems　　　　　　　　　　　　　　　
  Kai Shi; Yuichi Goto; Zhiliang Zhu; Jingde Cheng
  INTELLIGENT INFORMATION AND DATABASE SYSTEMS (ACIIDS 2013), PT I,, Volume：7802, Number：PART 1, First page：117, Last page：126, 2013, [Reviewed]
  This paper proposes a new type of emergency elevator evacuation systems, named anticipatory emergency elevator evacuation systems, which can detect and predict hazards in the emergency evacuation, and then dispatch the elevator cars anticipatorily, aiming to avoid hazards beforehand, thus to rescue more occupants and to shorten the evacuation time. This paper presents the proposed system's design, its prototype and evaluation. The novelty of the presented work is that it shows a new direction for developing emergency elevator evacuation systems.
  SPRINGER-VERLAG BERLIN, English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-642-36546-1_13
  DOI ID：10.1007/978-3-642-36546-1_13, ISSN：0302-9743, ORCID：10636972, Web of Science ID：WOS:000340589100013
• An Analysis of Software Supportable Tasks Related with ISO/IEC 15408　　　　　　　　　　　　　　　
  Ning Zhang; Ahmad Iqbal Hakim Suhaimi; Yuichi Goto; Jingde Cheng
  2013 9TH INTERNATIONAL CONFERENCE ON COMPUTATIONAL INTELLIGENCE AND SECURITY (CIS), First page：601, Last page：606, 2013, [Reviewed]
  From the perspective of information security engineering, ISO/IEC 15408, one of ISO/IEC security standards, plays an important role to ensure the whole security of an information/software system. ISO/IEC 15408 is a complex security standard which requires involvement of wide range of participants to perform a quite number of tasks as well as various documents. ISO/IEC 15408 is periodically reviewed and maintained to achieve ongoing improvement so that workflow of tasks and contents/format of documents related with the standard are changed according to changes of the standards. Consequently, it is difficult to do all of the tasks related with ISO/IEC 15408 without any supporting tools. However, there is no study to identify which tasks related with ISO/IEC 15408 can be supported by software tools. Indeed, no one makes clear what the tasks and participants exist. This paper presents the first analysis to identify all software supportable tasks related with ISO/IEC 15408. The paper enumerates all of the participants, documents, and tasks related with ISO/IEC 15408 and shows relationship among them, and identifies all software supportable tasks. The analysis and its results become a basis to construct an information security engineering environment based on ISO/IEC 15408 for ensuring the whole security of an information/software system.
  IEEE, English, International conference proceedings
  DOI：https://doi.org/10.1109/CIS.2013.132
  DOI ID：10.1109/CIS.2013.132, ORCID：14254540, SCOPUS ID：84900662221, Web of Science ID：WOS:000351209000125
• Continuous Functioning of Soft System Bus Based Centralized Persistent Computing Systems　　　　　　　　　　　　　　　
  Quazi Mahera Jabeen; Muhammad Anwarul Azim; Yuichi Goto; Jingde Cheng
  International Journal of New Computer Architectures and their Applications, Volume：2, Number：2, First page：362, Last page：381, Apr. 2012, [Reviewed]
  English, Scientific journal
• A truth maintenance system for epistemic programming environment　　　　　　　　　　　　　　　
  Yucihi Goto; Jingde Cheng
  Proceedings - 2012 8th International Conference on Semantics, Knowledge and Grids, SKG 2012, First page：1, Last page：8, 2012, [Reviewed], [Invited]
  Epistemic Programming was proposed as a novel program paradigm to program epistemic processes in scientific discovery, and an epistemic programming language and its implementation were also proposed and developed. The paradigm of Epistemic Programming regards conditionals as the subject of computing, takes primary epistemic operations as basic operations of computing, and regards epistemic processes as the subject of programming. In order to provide scientists with a high-level and general-purpose mechanism to deal with belief revision more easily in Epistemic Programming, this paper proposes a truth maintenance system for epistemic programming environments. At first, the paper analyzes features of a truth maintenance system for epistemic programming environment. Then, the paper gives a requirement analysis of the truth maintenance system, and shows a design of the truth maintenance system. The proposed truth maintenance system is suitable for epistemic programming environment, and can deal with replacement of logic systems underlying reasoning in epistemic processes. © 2012 IEEE.
  English, International conference proceedings
  DOI：https://doi.org/10.1109/SKG.2012.14
  DOI ID：10.1109/SKG.2012.14, SCOPUS ID：84872297135
• Development of a general-purpose E-testing server for ubiquitous test　　　　　　　　　　　　　　　
  Jumpei Suzuki; Yuichi Goto; Jingde Cheng
  Advances in Intelligent and Soft Computing, Volume：162, First page：797, Last page：803, 2012, [Reviewed]
  Test is a general and indispensable method, and widely used to assess people's achievement, ability, and char- acteristics in education, enterprise, medicine, and government. In recent years, various E-testing tools are developed ad hoc because purposes and procedures of tests are different from each other. However, an E-testing tool for general-purpose can be developed, and is demanded. Most tests have same processes, and a person or an organization may do several kinds of tests. This paper proposes ubiquitous test as a new E- service. Ubiquitous test is an E-testing service to provide users with E-testing services anytime and anywhere such that one can use E-testing servers without even thinking about them. The paper also presents a requirement analysis, architecture, and facilities for the general-purpose E-testing server for the ubiquitous test. © 2012 Springer-Verlag GmbH.
  English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-642-29455-6_107
  DOI ID：10.1007/978-3-642-29455-6_107, ISSN：1867-5662, SCOPUS ID：84866000883
• Evolutionary personal information partners for students studying in universities　　　　　　　　　　　　　　　
  Ryota Kuboniwa; Yuichi Goto; Jingde Cheng
  Advances in Intelligent and Soft Computing, Volume：162, First page：789, Last page：795, 2012, [Reviewed]
  In current information society, one can get huge amount of data easily and quickly. However, it is not so easy to extract useful information from huge amount of data. Undergraduate students and graduate students are not skillful with extracting useful information from huge date they got. They need a service to support their studying in a comprehensive way. Therefore, a service to help undergraduate students and graduate students should help their studying and extracting useful information from huge data they got. This paper proposes an evolutionary personal information partner for students studying in universities that can store and manage all its user's information related studying, and autonomously provide the user with advices about studying. Undergraduate students and graduate students can spend useful days in their life because the service the evolutionary personal information partner for studying in universities provides. © 2012 Springer-Verlag GmbH.
  English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-642-29455-6_106
  DOI ID：10.1007/978-3-642-29455-6_106, ISSN：1867-5662, SCOPUS ID：84865980078
• Internationalization of ENQUETE-BAISE: A general-purpose E-questionnaire server for ubiquitous questionnaire　　　　　　　　　　　　　　　
  Jingzhou Wang; Yuichi Goto; Jingde Cheng
  Advances in Intelligent and Soft Computing, Volume：162, First page：781, Last page：787, 2012, [Reviewed]
  Ubiquitous questionnaire is to provide users with E-questionnaire services anytime and anywhere such that one can use E-questionnaire servers without even thinking about them. A general-purpose E-questionnaire server for ubiquitous questionnaire, named "ENQUETE-BAISE", was proposed. It deals with not only E-questionnaire, but also E-voting and E-testing. On the other hand, the most intrinsic feature of ubiquitous questionnaire is to allow anyone to execute any kind of questionnaires anytime anywhere such that any respondent can answer questionnaires anytime anywhere. ENQUETE- BAISE should provide an environment that any user can do E-questionnaire, E-voting, or E-testing in his/her well-used locale. However, current ENQUETE-BAISE cannot provide such an environment. This paper proposes a mechanism to deal with internationalization of E-questionnaire, E-voting, and E-testing, and shows internationalization of ENQUETE- BAISE. The proposed mechanism is not ad-hoc such that it is independent of functional requirements of E-questionnaire, E-voting, and E-testing. Thus, we can use the mechanism continuously if ENQUETE-BAISE becomes more complex or more functional. © 2012 Springer-Verlag GmbH.
  English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-642-29455-6_105
  DOI ID：10.1007/978-3-642-29455-6_105, ISSN：1867-5662, SCOPUS ID：84865976098
• ISEC: An information security engineering cloud　　　　　　　　　　　　　　　
  Liqing Xu; Kai Shi; Yuichi Goto; Jingde Cheng
  ICSESS 2012 - Proceedings of 2012 IEEE 3rd International Conference on Software Engineering and Service Science, First page：750, Last page：753, 2012, [Reviewed]
  ISEE was proposed as an information security engineering environment that supports continuous and consistent design, development, management and maintenance of security facilities of target systems, based on ISO/IEC security standards. However, the current ISEE only provides services passively, i.e., it can only response to users' explicit requests, but cannot provide useful services to users actively. In order to make ISEE more practical, it is a challenge to provide active services, which can give useful services to users actively in advance but do not give users undesired services. To this end, this paper proposes an information security engineering cloud (ISEC), that has all functions of ISEE, and moreover, provides active services to its users. This paper presents the basic ideas, requirements, design, and implementation issues of ISEC. © 2012 IEEE.
  English, International conference proceedings
  DOI：https://doi.org/10.1109/ICSESS.2012.6269575
  DOI ID：10.1109/ICSESS.2012.6269575, SCOPUS ID：84866485274
• A supporting tool for creating and maintaining security targets according to ISO/IEC 15408　　　　　　　　　　　　　　　
  Gefei Sun; Kenichi Yajima; Junichi Miura; Kai Shi; Yuichi Goto; Jingde Cheng
  ICSESS 2012 - Proceedings of 2012 IEEE 3rd International Conference on Software Engineering and Service Science, First page：745, Last page：749, 2012, [Reviewed]
  To acquire the certification according to ISO/IEC 15408 for a target system, it is necessary to create a security target (ST) which specifies security facilities of the system. Creating STs is not an easy task for developers because they do not know how to create STs well, even if they know the security facilities. Meanwhile, STs should be maintained continuously to keep a target system secure. Maintaining STs is not easy as same as creating STs. However, there is no tool to support developers and maintainers to create and maintain STs so far. This paper presents a supporting tool according to ISO/IEC 15408, named ST-Editor. ST-Editor tells users what should be described and how they should be described in STs and provides a helpful and secure editing and maintaining environment of STs. © 2012 IEEE.
  English, International conference proceedings
  DOI：https://doi.org/10.1109/ICSESS.2012.6269574
  DOI ID：10.1109/ICSESS.2012.6269574, SCOPUS ID：84866498553
• Generation of system dependence nets for Ada 2005 programs
  Bo Wang; Kai Shi; Yuichi Goto; Jingde Cheng
  CSAE 2012 - Proceedings, 2012 IEEE International Conference on Computer Science and Automation Engineering, Volume：3, First page：401, Last page：406, 2012, [Reviewed]
  System dependence net is a formal model to explicitly represent program dependences in a concurrent program which consists of multiple procedures. It is useful for development and maintenance of concurrent programs, such as program slicing, testing, debugging, and complexity measuring. A system dependence net generator for Ada 95 was proposed and developed. It cannot be used for Ada 2005 programs because Ada 2005 has a lot of changes from Ada 95. There is no study about how to generate system dependence nets of Ada 2005 programs until now. This paper proposes a method to generate system dependence nets of Ada 2005 programs by improving already proposed method for Ada 95. © 2012 IEEE.
  English, International conference proceedings
  DOI：https://doi.org/10.1109/CSAE.2012.6272981
  DOI ID：10.1109/CSAE.2012.6272981, SCOPUS ID：84867050937
• Dynamic reconfiguration of persistent computing systems based on soft system bus　　　　　　　　　　　　　　　
  Jingde Cheng; Masami Someya; Koichi Nanashima; Yuichi Goto
  CSAE 2012 - Proceedings, 2012 IEEE International Conference on Computer Science and Automation Engineering, Volume：2, First page：368, Last page：372, 2012, [Reviewed]
  Anytime reconfigurability of computing systems is indispensable to persistent computing as well as ubiquitous/pervasive/cloud computing. To require that a computing system function continuously anytime entails that the computing system has to be reconfigured dynamically during its continuous running. This paper shows our approach to dynamic reconfiguration of persistent computing systems constructed based on soft system buses. The paper presents a requirement analysis for the dynamic reconfiguration of persistent computing systems based on soft system buses, proposes an architecture of persistent computing systems based on soft system buses that satisfied the requirements, and presents some implementation issues. © 2012 IEEE.
  English, International conference proceedings
  DOI：https://doi.org/10.1109/CSAE.2012.6272794
  DOI ID：10.1109/CSAE.2012.6272794, SCOPUS ID：84867053073
• Practical usage of freeencal: An automated forward reasoning engine for general-purpose
  Yuichi Goto; Hongbiao Gao; Takahiro Tsuji; Jingde Cheng
  Proceedings - International Conference on Machine Learning and Cybernetics, Volume：5, First page：1878, Last page：1883, 2012, [Reviewed]
  Forward reasoning engine is a computer program to automatically draw new conclusions by repeatedly applying inference rules. An automated forward reasoning engine for general-purpose, named FreeEnCal, has been proposed and developed. Then, to improving its performance and generality, fast algorithms and a general reasoning algorithm are proposed and implemented, but separately. Until now, there is no practical implementation of FreeEnCal that are adopted those algorithms. This paper shows the practical implementation of FreeEnCal and its practical usage. We can expect to use the practical FreeEnCal for an alternative tool to prove something, an enumeration tool by using forward deduction, a web service of automated forward reasoning. © 2012 IEEE.
  English, International conference proceedings
  DOI：https://doi.org/10.1109/ICMLC.2012.6359662
  DOI ID：10.1109/ICMLC.2012.6359662, ISSN：2160-133X, ORCID：10636973, SCOPUS ID：84871584831
• Formal analysis of cryptographic protocols by reasoning based on deontic relevant logic: A case study in Needham-Schroeder Shared-Key protocol
  Kazunori Wagatsuma; Yuichi Goto; Jingde Cheng
  Proceedings - International Conference on Machine Learning and Cybernetics, Volume：5, First page：1866, Last page：1871, 2012, [Reviewed]
  Formal analysis of cryptographic protocols is necessary to assure security before using it. In traditional approaches, analysts have to specify security goals or necessary conditions of the analysis firstly. However, it is difficult to specify all security goals or necessary conditions. A reasoning approach without the problem was proposed, but its concrete method is not established. In this paper, as the first step to elaborate the reasoning approach of cryptographic protocols, we analyzed Needham-Schroeder Shared-Key protocol by reasoning based on deontic relevant logic. By the case study, we show that the reasoning approach can find vulnerability of the cryptographic protocol as well as traditional approach, and can expect to find new vulnerability that has not been recognized. Then, we discuss about the concrete method for formal analysis of cryptographic protocols by the reasoning approach. © 2012 IEEE.
  English, International conference proceedings
  DOI：https://doi.org/10.1109/ICMLC.2012.6359660
  DOI ID：10.1109/ICMLC.2012.6359660, ISSN：2160-133X, ORCID：10636974, SCOPUS ID：84871548465
• Automated theorem finding by forward deduction based on strong relevant logic: A case study in NBG set theory
  Hongbiao Gao; Kai Shi; Yuichi Goto; Jingde Cheng
  Proceedings - International Conference on Machine Learning and Cybernetics, Volume：5, First page：1859, Last page：1865, 2012, [Reviewed]
  The problem of automated theorem finding is one of 33 basic research problems in automated reasoning which was originally proposed by Wos in 1988, and it is still an open problem. To solve the problem, a forward deduction approach based on the strong relevant logics was proposed. To verify the effectiveness of the approach, this paper presents a case study of automated theorem finding in NBG set theory by forward deduction based on the strong relevant logics. The ultimate goal of automated theorem finding in NBG set theory is to find new and interesting theorems. As the first step, this case study tries to do "rediscovery" in NBG set theory, i.e., to deduce already proved theorems from axioms, definitions and /or other theorems of NBG set theory. However, from the viewpoint of the mechanism of deducing theorems, "re-discovery" is as same as "discovery". The paper shows several known theorems rediscovered successfully by the approach. The paper also shows issues of the approach for real "discovery". © 2012 IEEE.
  English, International conference proceedings
  DOI：https://doi.org/10.1109/ICMLC.2012.6359659
  DOI ID：10.1109/ICMLC.2012.6359659, ISSN：2160-133X, ORCID：10636975, SCOPUS ID：84871587655
• An Engineering Environment for Supporting Information Security Management Systems　　　　　　　　　　　　　　　
  Ahmad Iqbal Hakim Suhaimi; Yuichi Goto; Jingde Cheng
  COMPUTER APPLICATIONS FOR SECURITY, CONTROL AND SYSTEM ENGINEERING, Volume：339, First page：30, Last page：37, 2012, [Reviewed]
  Information Security Management Systems (ISMSs) have been playing an important role to help organizations managing their information securely. However, organizations facing many challenges in from establishment phase to optimization phase of ISMSs because organizations have to perform a lot of tasks with various participants and manage a vast amount of documents. As a result, it is difficult for an organization to establish and maintain a good and effective ISMS. This paper proposes an engineering environment to support organizations with ISMSs which is an engineering environment that integrating various support tools to provide organizations with comprehensives facilities to perform all tasks in ISMS life cycle processes consistently and continuously based on ISO/IEC 27000 series standards.
  SPRINGER-VERLAG BERLIN, English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-642-35264-5_5
  DOI ID：10.1007/978-3-642-35264-5_5, ISSN：1865-0929, ORCID：10636976, Web of Science ID：WOS:000313300800005
• Providing Users With Suitable Services of Information Security Engineering Cloud Based on ISO/IEC 15408　　　　　　　　　　　　　　　
  Liqing Xu; Bo Wang; Ning Zhang; Yuichi Goto; Jingde Cheng
  PROCEEDINGS OF 2013 IEEE 4TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND SERVICE SCIENCE (ICSESS), First page：321, Last page：325, 2012, [Reviewed]
  Information security engineering cloud (ISEC) should provide a wide range of services for its users to ensure the whole security of their target information/software systems. ISO/IEC 15408, as one of the most important international standards, plays an important role to ensure whole security of target information/software systems, and therefore, has been adopted as the core standard in ISEC. There are various services provided by ISEC based on ISO/IEC 15408. As a result, it is difficult for the users to find suitable services. However, there is no analysis about how to support users to find suitable services according to their roles and tasks. This paper identifies, classifies, and combines all services of ISEC based on ISO/IEC 15408. According to our analysis results and using supporting tools we are developing, ISEC based on ISO/IEC 15408 can provide efficient and satisfactory services to its users.
  IEEE, English, International conference proceedings
  DOI：https://doi.org/10.1109/ICSESS.2013.6615315
  DOI ID：10.1109/ICSESS.2013.6615315, ISSN：2327-0594, ORCID：14254537, SCOPUS ID：84890027993, Web of Science ID：WOS:000346301300073
• New Types of Program Dependences and Interprocedural Relations in Ada 2012 Programs　　　　　　　　　　　　　　　
  Bo Wang; Yuichi Goto; Jingde Cheng
  PROCEEDINGS OF 2013 IEEE 4TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND SERVICE SCIENCE (ICSESS), First page：718, Last page：723, 2012, [Reviewed]
  System dependence net is a formal model to explicitly represent program dependences and interprocedural relations in a concurrent program with multiple procedures. It is useful for development and maintenance of concurrent programs, such as program slicing, testing, debugging, and complexity measuring. By now, although system dependence nets for Ada 95 and Ada 2005 programs were proposed respectively, they cannot be used for Ada 2012 programs, because Ada 2012 has a lot of changes and extensions from Ada 2005. As the first step to extend the current model of system dependence nets for Ada 2012 programs, it is indispensable to identify all new program dependences and interprocedural relations in Ada 2012 programs. This paper presents some new types of program dependences and interprocedural relations in Ada 2012 programs, and shows their real examples.
  IEEE, English, International conference proceedings
  DOI：https://doi.org/10.1109/ICSESS.2013.6615407
  DOI ID：10.1109/ICSESS.2013.6615407, ISSN：2327-0594, ORCID：14254539, SCOPUS ID：84890082551, Web of Science ID：WOS:000346301300165
• An Anticipatory Reasoning-Reacting System for Defending Against Malice Anticipatorily　　　　　　　　　　　　　　　
  Kai Shi; Bo Wang; Yuichi Goto; Zhiliang Zhu; Jingde Cheng
  PROCEEDINGS OF 2013 IEEE 4TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND SERVICE SCIENCE (ICSESS), First page：732, Last page：737, 2012, [Reviewed]
  Today, information security of information systems is no longer about confidentiality, integrity and availability, but about ensuring that the systems are predictably dependable in the face of all sorts of malice. Although intrusion detection systems (IDS) make big progress on defending against computing malice, there is still a gap between current IDSs and ideal malice defense systems. On the other hand, anticipatory reasoning-reacting systems (ARRS) were proposed as a high secure system with the ability to defend against malice anticipatorily, however, until now, there is no concrete implementation of ARRS for security, as well as no evidence showing the practical usefulness of anticipatory computing for security. As a step towards to ideal secure systems, we designed and implemented an ARRS for malice defense, which can adapt to different application by configuring different information source, anticipatory model, and anticipatory actions. We also evaluated our system by KDD99 dataset and a case study of web server. This paper proposes what features ideal malice defense systems should have, points out the gap between current IDSs and ideal malice defense systems, shows why some advantages of ARRSs could contribute ideal malice defense systems, and presents and evaluates a practical implementation of ARRS for security.
  IEEE, English, International conference proceedings
  DOI：https://doi.org/10.1109/ICSESS.2013.6615410
  DOI ID：10.1109/ICSESS.2013.6615410, ISSN：2327-0594, ORCID：14254538, SCOPUS ID：84890016231, Web of Science ID：WOS:000346301300168
• Security Analysis of Peer-to-Peer based Soft System Bus Based System　　　　　　　　　　　　　　　
  Muhammad Anwarul Azim; Yuichi Goto; Jingde Cheng
  International Journal of Computer Science and Network Security, Volume：11, Number：2, First page：164, Last page：172, Feb. 2011, [Reviewed]
  English, Scientific journal
• A Design of Centralized Persistent Computing System　　　　　　　　　　　　　　　
  Quazi Mahera Jabeen; Muhammad Anwarul Azim; Yuichi Goto; Jingde Cheng
  INFORMATICS ENGINEERING AND INFORMATION SCIENCE, PT I, Volume：251, First page：604, Last page：617, 2011, [Reviewed]
  Persistent Computing Systems (PCSs) were proposed as a new generation reactive systems that are dependable and dynamically adaptive. They provide services to their users anytime and anywhere during system maintenance, upgrade, reconfiguration and even during various attacks. PCSs have demand not only for distributed systems but also centralized systems. To implement PCSs, Soft System Bus (SSB) based systems were proposed. Although a design and implementation method of SSB-based systems exists for distributed PCSs, any requirement analysis, design, and implementation method of SSB-based centralized PCSs (SSB-based CPCSs) have not been addressed yet. This paper presents requirement analysis of SSB-based CPCS, proposes its design, and investigates available techniques to realize SSB-based CPCS.
  SPRINGER-VERLAG BERLIN, English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-642-25327-0_51
  DOI ID：10.1007/978-3-642-25327-0_51, ISSN：1865-0929, Web of Science ID：WOS:000310491700051
• A Systematic Management Method of ISO Information Security Standards for Information Security Engineering Environments　　　　　　　　　　　　　　　
  Ahmad Iqbal Hakim Suhaimi; Takashi Manji; Yuichi Goto; Jingde Cheng
  INFORMATICS ENGINEERING AND INFORMATION SCIENCE, PT I, Volume：251, First page：370, Last page：384, 2011, [Reviewed]
  An ideal secure information system is not only to keep enough security strength of all components of a target system, but also to ensure all tasks in software life cycle process are done appropriately. Under the consideration, information security engineering environments that integrate various tools to support the tasks are proposed. On the other hand, it is difficult to define generally accepted security strength and its evaluation criteria. ISO information security standards, which regulate various information security related contents are expected, can be used as criteria for the purpose, and should be provided as databases to be used from the tools. However, because standards are always changed and their contents are different from each others, it is difficult to design and manage the databases. This paper proposes a systematic management for information security engineering environments that ensure safety in software life cycle based on the standards.
  SPRINGER-VERLAG BERLIN, English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-642-25327-0_32
  DOI ID：10.1007/978-3-642-25327-0_32, ISSN：1865-0929, Web of Science ID：WOS:000310491700032
• Practical implementation of EPLAS: An Epistemic Programming Language for all scientists　　　　　　　　　　　　　　　
  Wencheng Fang; Isao Takahashi; Yuichi Goto; Jingde Cheng
  Proceedings - International Conference on Machine Learning and Cybernetics, Volume：2, First page：608, Last page：616, 2011, [Reviewed]
  Epistemic Programming was proposed as a new programming paradigm for scientists to program their epistemic processes in scientific discovery. To provide such epistemic programming environment, the concept and some fundamental ideas of EPLAS, an Epistemic Programming Language for All Scientists, were proposed. As a programming language, EPLAS must have a practical implementation. However there does not exist such implementation. This paper describes the requirements of both EPLAS language specification and its implementation. Based on those requirements, the paper presents an interpreter of EPLAS which is the first epistemic programming environment. Our implementation can be used to program the epistemic processes of some scientific thinking methods. © 2011 IEEE.
  English, International conference proceedings
  DOI：https://doi.org/10.1109/ICMLC.2011.6016780
  DOI ID：10.1109/ICMLC.2011.6016780, ISSN：2160-133X, SCOPUS ID：80155176195
• Development and Maintenance Environment for Anticipatory Reasoning-Reacting Systems　　　　　　　　　　　　　　　
  Yuichi Goto; Ryota Kuboniwa; Jingde Cheng
  International Journal of Computing Anticipatory Systems, Volume：24, First page：61, Last page：72, Dec. 2010, [Reviewed]
  English, Scientific journal
• Fast Anticipatory Reasoning for Computing Anticipatory Systems　　　　　　　　　　　　　　　
  Takahiro Koh; Yuichi Goto; Jingde Cheng
  International Journal of Computing Anticipatory Systems, Volume：24, First page：42, Last page：53, Dec. 2010, [Reviewed]
  English, Scientific journal
• A Fast Algorithm for Derivation Process in Forward Reasoning Engines, International Journal of Computational Science　　　　　　　　　　　　　　　
  Takahiro Koh; Yuichi Goto; Jingde Cheng
  Global Information Publisher, Volume：4, Number：3, First page：219, Last page：231, Jun. 2010, [Reviewed]
  English, Scientific journal
• Development of ISEE: An Information Security Engineering Environment　　　　　　　　　　　　　　　
  Jingde Cheng; Yuichi Goto; Daisuke Horie; Junichi Miura; Toshio Kasahara; Ahmad Iqbal
  2009 IEEE INTERNATIONAL SYMPOSIUM ON PARALLEL AND DISTRIBUTED PROCESSING WITH APPLICATIONS, PROCEEDINGS, First page：505, Last page：510, 2009, [Reviewed]
  Security Engineering has some features that are intrinsically different from Software (Reliability) Engineering. Traditional software engineering environments are not adequate and effective for designing, developing, managing, and maintaining secure software systems. This paper presents our development of ISEE, an information security engineering environment we are developing, that integrates various tools and provides comprehensive facilities to support design, development, management, and maintenance of security facilities of information/software systems continuously and consistently, and guides and helps all users to perform their tasks regularly according to ISO/IEC security standards. ISEE is the first real information security engineering environment.
  IEEE COMPUTER SOC, English, International conference proceedings
  DOI：https://doi.org/10.1109/ISPA.2009.107
  DOI ID：10.1109/ISPA.2009.107, Web of Science ID：WOS:000275653700072
• Information Assurance, Privacy, and Security in Ubiquitous Questionnaire　　　　　　　　　　　　　　　
  Yuichi Goto; Jingde Cheng
  FCST 2009: PROCEEDINGS OF THE 4TH INTERNATIONAL CONFERENCE ON FRONTIER OF COMPUTER SCIENCE AND TECHNOLOGY, First page：619, Last page：624, 2009, [Reviewed]
  Ubiquitous questionnaire is to provide users with E-questionnaire services anytime and anywhere such that one can use E-questionnaire servers without even thinking about them. An E-questionnaire server for ubiquitous questionnaire should provide guarantees to satisfy any user-specified requirement on information assurance, privacy, and security because some questionnaires may concern organization secrets as well as personal privacy, and some questionnaires such as E-voting or E-testing must impose restrictions on and provide assurance to respondents, voters, and/or testees. Until now, there is no detail requirement analysis for information assurance, privacy, and security in ubiquitous questionnaire. To implement an questionnaire server server for ubiquitous questionnaire, this paper presents a requirement analysis for information assurance, privacy, and security in ubiquitous questionnaire. The paper identifies all participants and their information assets in ubiquitous questionnaire with a general purpose E-questionnaire server that can be used not only an E-questionnaire server but also an E-voting server and an E-testing server, gives a threat analysis of and a requirement analysis for information assurance, privacy, and security, and investigates technical issues for implementing facilities satisfied the requirements.
  IEEE COMPUTER SOC, English, International conference proceedings
  DOI：https://doi.org/10.1109/FCST.2009.111
  DOI ID：10.1109/FCST.2009.111, Web of Science ID：WOS:000276838500093
• A Database System for Effective Utilization of ISO/IEC 27002　　　　　　　　　　　　　　　
  Ahmad Iqbal; Daisuke Horie; Yuichi Goto; Jingde Cheng
  FCST 2009: PROCEEDINGS OF THE 4TH INTERNATIONAL CONFERENCE ON FRONTIER OF COMPUTER SCIENCE AND TECHNOLOGY, First page：607, Last page：612, 2009, [Reviewed]
  ISO/IEC 27002 is an international standard for information security management. Although many organizations need to manage their information systems according to ISO/IEC 27002, ISO/IEC 27002 is not convenient for users to retrieve terms, definitions, and security controls and to make documents for information security management because the ISO/IEC 27002 is distributed only in form of booklet or PDF. On the other hand, ISEE, an information security engineering environment, has been proposed to support all tasks in from requirement analysis to maintenance of security facilities of software/information systems. ISEDS, an information security engineering database system, as a main component of ISEE, is planed manage all ISO standards related with information security and their concerning documents. This paper presents a database system for effective utilization of ISO/IEC 27002 that is obtained by adding ISO/IEC 27002 and related documents into ISEDS. The paper analyzes usages of ISO/IEC 27002, gives requirement analysis of the database system, presents a design and construction of the database system, and shows a usage example. The paper also investigates a systematic method to construct databases of ISO standards for information security in ISEDS.
  IEEE COMPUTER SOC, English, International conference proceedings
  DOI：https://doi.org/10.1109/FCST.2009.88
  DOI ID：10.1109/FCST.2009.88, Web of Science ID：WOS:000276838500091
• Development of ISEE: An Information Security Engineering Environment　　　　　　　　　　　　　　　
  Daisuke Horie; Yuichi Goto; Jingde Cheng
  PROCEEDINGS OF THE SECOND INTERNATIONAL SYMPOSIUM ON ELECTRONIC COMMERCE AND SECURITY, VOL I, First page：338, Last page：342, 2009, [Reviewed]
  This paper presents a requirement analysis, design, and implementation of ISEE: an information security engineering environment. ISEE integrates various tools and functions for supporting continuous and consistent design, development, management, maintenance, and abolition of security facilities of information systems with high security requirements, and forces users to perform their tasks according to ISO standards and a regular sequence. We defined requirements for ISEE to achieve continuous and consistent design, development, management, maintenance, and abolition of security facilities. We also designed ISEE according to the requirements, and implemented some tools of ISEE. Users of ISEE can ensure the whole security of a system by continuously and consistently performing their tasks.
  IEEE COMPUTER SOC, English, International conference proceedings
  DOI：https://doi.org/10.1109/ISECS.2009.243
  DOI ID：10.1109/ISECS.2009.243, Web of Science ID：WOS:000275129000070
• ISEE: AN INFORMATION SECURITY ENGINEERING ENVIRONMENT
  Jingde Cheng; Yuichi Goto; Daisuke Horie
  SECRYPT 2009: PROCEEDINGS OF THE INTERNATIONAL CONFERENCE ON SECURITY AND CRYPTOGRAPHY, First page：395, Last page：400, 2009, [Reviewed]
  Security Engineering has some features that are intrinsically different from Software (Reliability) Engineering. Traditional software engineering environments are not adequate and effective for designing, developing, managing, and maintaining secure software systems. This position paper presents ISEE, an information security engineering environment we are developing, that integrates various tools and provides comprehensive facilities to support design, development, management, and maintenance of security facilities of information/software systems continuously and consistently, and guides and helps all users to perform their tasks regularly according to ISO/IEC security standards. The paper presents the basic ideas on development of ISEE, basic requirements for ISEE, and a design of ISEE. ISEE is the first real information security engineering environment.
  INSTICC-INST SYST TECHNOLOGIES INFORMATION CONTROL & COMMUNICATION, English, International conference proceedings
  Web of Science ID：WOS:000282088500060
• Development of a Decision-Maker in an Anticipatory Reasoning-Reacting System for Terminal Radar Control　　　　　　　　　　　　　　　
  Natsumi Kitajima; Yuichi Goto; Jingde Cheng
  HYBRID ARTIFICIAL INTELLIGENCE SYSTEMS, Volume：5572, First page：68, Last page：76, 2009, [Reviewed]
  Terminal radar control is more and more complex in recent years. To reduce human errors in terminal radar control, an automatic system to support conflict detection and conflict resolution is required for reliable and safe terminal radar control. An anticipatory reasoning-reacting system for terminal radar control is a hopeful candidate for such systems. This paper proposes a methodology of decision-making in an anticipatory reasoning-reacting system for terminal radar control, presents a prototype of decision-maker, and shows that it can make appropriate decisions in anticipatory reasoning-reacting system for terminal radar control.
  SPRINGER-VERLAG BERLIN, English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-642-02319-4_9
  DOI ID：10.1007/978-3-642-02319-4_9, ISSN：0302-9743, Web of Science ID：WOS:000267794600009
• A New Model of Software Life Cycle Processes for Consistent Design, Development, Management, and Maintenance of Secure Information Systems　　　　　　　　　　　　　　　
  Daisuke Horie; Toshio Kasahara; Yuichi Goto; Jingde Cheng
  PROCEEDINGS OF THE 8TH IEEE/ACIS INTERNATIONAL CONFERENCE ON COMPUTER AND INFORMATION SCIENCE, First page：897, Last page：902, 2009, [Reviewed]
  This paper presents a new model of software life cycle processes for consistent design, development, management, maintenance, and abolition of secure information systems. The model clearly specifies tasks for engineering security facilities, standards underlying the tasks, and a regular sequence of the tasks. We defined the model according to ISO/IEC 12207 and other ISO standards related to security. The model can be customized as software life cycle processes for various systems with particular purposes. Users of software life cycle processes according to the model can continuously and consistently design, develop, manage, maintain, and abrogate secure information systems whose security is ensured by ISO standards.
  IEEE COMPUTER SOC, English, International conference proceedings
  DOI：https://doi.org/10.1109/ICIS.2009.175
  DOI ID：10.1109/ICIS.2009.175, Web of Science ID：WOS:000273558200153
• GEST: A Generator of ISO/IEC 15408 Security Target Templates　　　　　　　　　　　　　　　
  Daisuke Horie; Kenichi Yajima; Noor Azimah; Yuichi Goto; Jingde Cheng
  COMPUTER AND INFORMATION SCIENCE 2009, Volume：208, First page：149, Last page：158, 2009, [Reviewed]
  This paper presents a generator of ISO/IEC 15408 security target templates, named "GEST," that can automatically generate security target templates for target information systems from evaluated and certified security targets. GEST can choose certified security targets resembling target system according to keywords inputted by users, and detect and correct discordance of templates. By using GEST, designers with a little experience can easily get security target templates as the basis to create security targets of target systems.
  SPRINGER, English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-642-01209-9
  DOI ID：10.1007/978-3-642-01209-9, ISSN：1860-949X, Web of Science ID：WOS:000265819400014
• An Improvement of REM: A Replication Oriented Event-based Middleware　　　　　　　　　　　　　　　
  Youcheng Chen; Mohammad Reza Selim; Yuichi Goto; Jingde Cheng
  2009 INTERNATIONAL CONFERENCE ON AVAILABILITY, RELIABILITY, AND SECURITY (ARES), VOLS 1 AND 2, First page：641, Last page：646, 2009, [Reviewed]
  Existing publish-subscribe middlewares do not provide reliability guarantees about the event delivery, though the guarantees are necessary in an unstable communication environment. To provide the reliability guarantees, we have proposed a large-scale replication oriented event-based middleware, named "REM", over structured peer to peer network. However, the present REM cannot detect loss of events in some cases. In this paper, we present an improved design of REM which can detect and report failures of event delivery, and recover the lost events.
  IEEE, English, International conference proceedings
  DOI：https://doi.org/10.1109/ARES.2009.161
  DOI ID：10.1109/ARES.2009.161, Web of Science ID：WOS:000270612000093
• FORVEST: A Support Tool for Formal Verification of Security Specifications with ISO/IEC 15408　　　　　　　　　　　　　　　
  Kenichi Yajima; Shoichi Morimoto; Daisuke Horie; Noor Sheila Azreen; Yuichi Goto; Jingde Cheng
  2009 INTERNATIONAL CONFERENCE ON AVAILABILITY, RELIABILITY, AND SECURITY (ARES), VOLS 1 AND 2, First page：624, Last page：+, 2009, [Reviewed]
  It is very important to formally verify security specifications of information systems for ensuring their security. Thus we have proposed a formal verification method of security specifications with ISO/IEC 15408. However to use the method, verifiers have to be familiar with Z notation, linear temporal logic, NuSMV input language, theorem proving, model checking, and ISO/IEC 15408. Moreover, the verifiers also have to prepare some tools supporting the formal verification. Therefore, the verifiers cannot utilize the method easily. To easily verify security specifications based on the method, this paper presents a support tool for the method, named "FORVEST". FORVEST supports the verifiers by guiding the verifiers appropriately and providing information of Z notation, linear temporal logic, theorem proving, model checking, and ISO/IEC 15408 when they are needed. FORVEST also provides an environment where verifiers can access and use tools of model checking and theorem proving through a Web browser By using FORVEST, verifiers can easily perform the formal verification.
  IEEE, English, International conference proceedings
  DOI：https://doi.org/10.1109/ARES.2009.74
  DOI ID：10.1109/ARES.2009.74, Web of Science ID：WOS:000270612000090
• Continuous Reactability of Persistent Computing Systems　　　　　　　　　　　　　　　
  Yuichi Goto; Takumi Endo; Jingde Cheng
  Volume：20, First page：219, Last page：229, Dec. 2008, [Reviewed]
  English, Scientific journal
• A Deontic Relevant Logic Approach to Reasoning about Actions in Computing Anticipatory Systems　　　　　　　　　　　　　　　
  Natsumi Kitajima; Shisuke Nara; Yuichi Goto; Jingde Cheng
  Volume：20, First page：177, Last page：190, Dec. 2008, [Reviewed]
  English, Scientific journal
• A Low Cost and Resilient Message Queuing Middleware　　　　　　　　　　　　　　　
  Mohammad Reza Selim; Yuichi Goto; Jingde Cheng
  Volume：8, Number：8, First page：225, Last page：237, Aug. 2008, [Reviewed]
  English, Scientific journal
• A fast duplication checking algorithm for forward reasoning engines　　　　　　　　　　　　　　　
  Takahiro Koh; Yuichi Goto; Jingde Cheng
  KNOWLEDGE-BASED INTELLIGENT INFORMATION AND ENGINEERING SYSTEMS, PT 2, PROCEEDINGS, Volume：5178, First page：499, Last page：507, 2008, [Reviewed]
  A forward reasoning engine capable of relevant reasoning is an indispensable component in many advanced knowledge-based systems with purposes of discovery or prediction. Any forward reasoning engine has to deal with duplication checking of intermediate results that is the most time-consuming process in forward reasoning. Therefore, to decrease execution time of forward reasoning engines is a crucial issue for their successful applications. This paper presents a fast; algorithm for duplication checking process in forward reasoning engines, analyzes its time and space complexities, and shows its effectiveness by some experimental results.
  SPRINGER-VERLAG BERLIN, English, International conference proceedings
  ISSN：0302-9743, Web of Science ID：WOS:000259394400062
• Anticipatory Reasoning about Mobile Objects in Anticipatory Reasoning-Reacting Systems　　　　　　　　　　　　　　　
  Jingde Cheng; Yuichi Goto; Natsumi Kitajima
  COMPUTING ANTICIPATORY SYSTEMS, Volume：1051, First page：244, Last page：254, 2008, [Reviewed]
  Anticipatory reasoning-reacting systems dealing with mobile objects must concern not only the notion of time but also the notion of space. To design and develop such anticipatory reasoning-reacting systems, we need to consider not only linear (total order) time but also branching (partial order) time, not only plane (two-dimensional) space but also solid (three-dimensional) space. To specify, verify, and reason about mobile objects in various anticipatory reasoning-reacting systems, we need a right fundamental logic system to provide us with a criterion of logical validity for reasoning as well as a formal representation and specification language. This paper proposes a new family of three-dimensional spatio-temporal relevant logics as a hopeful candidate for the fundamental logic.
  AMER INST PHYSICS, English, International conference proceedings
  DOI：https://doi.org/10.1063/1.3020663
  DOI ID：10.1063/1.3020663, ISSN：0094-243X, Web of Science ID：WOS:000262094700021
• A fast duplication checking algorithm for forward reasoning engines　　　　　　　　　　　　　　　
  Takahiro Koh; Yuichi Goto; Jingde Cheng
  Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Volume：5178, Number：2, First page：499, Last page：507, 2008, [Reviewed]
  A forward reasoning engine capable of relevant reasoning is an indispensable component in many advanced knowledge-based systems with purposes of discovery or prediction. Any forward reasoning engine has to deal with duplication checking of intermediate results that is the most time-consuming process in forward reasoning. Therefore, to decrease execution time of forward reasoning engines is a crucial issue for their successful applications. This paper presents a fast algorithm for duplication checking process in forward reasoning engines, analyzes its time and space complexities, and shows its effectiveness by some experimental results. © 2008 Springer-Verlag Berlin Heidelberg.
  English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-540-85565-1-62
  DOI ID：10.1007/978-3-540-85565-1-62, ISSN：0302-9743, SCOPUS ID：57749205896
• A general forward reasoning algorithm for various logic systems with different formalizations　　　　　　　　　　　　　　　
  Yuichi Goto; Takahiro Koh; Jingde Cheng
  KNOWLEDGE-BASED INTELLIGENT INFORMATION AND ENGINEERING SYSTEMS, PT 2, PROCEEDINGS, Volume：5178, First page：526, Last page：535, 2008, [Reviewed]
  A forward reasoning engine with general-purpose should he able to devil with various logic systems with different formalizations and various formal theories based oil the logic systems, and to perform deductive, inductive, and abductive reasoning based oil the logic systems. This paper presents a general forward reasoning algorithm for various logic systems formalized as Hilbert, style axiomatic systems, Gentzen natural deduction systems, or Gentzen sequent calculus systems, and its, implementation in FreeEnCal, a forward reasoning engine with general-purpose, that, we are developing.
  SPRINGER-VERLAG BERLIN, English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-540-85565-1
  DOI ID：10.1007/978-3-540-85565-1, ISSN：0302-9743, Web of Science ID：WOS:000259394400065
• Ensuring reliability and availability of soft system bus　　　　　　　　　　　　　　　
  Mohammad Reza Selim; Yuichi Goto; Jingde Cheng
  Proceedings - The 2nd IEEE International Conference on Secure System Integration and Reliability Improvement, SSIRI 2008, First page：52, Last page：59, 2008, [Reviewed]
  Many critical systems require high reliability and availability even when the systems are being maintained or upgraded. Soft System Bus (SSB) is the middleware for such systems. A conceptual architecture of SSB based on structured p2p network was proposed in our previous work. But, how high reliability and availability can be ensured was left unsolved. In this paper, we propose mechanisms to solve reliability and availability issues and analyze the effect of failures/arrivals of nodes on availability. Based on our solution, a SSB based system has been built in a simulated environment and the availability of SSB has been evaluated. Our results show that it is possible to achieve almost four nine availability in a reasonably dynamic environment assuring reliable delivery. © 2008 IEEE.
  English, International conference proceedings
  DOI：https://doi.org/10.1109/SSIRI.2008.51
  DOI ID：10.1109/SSIRI.2008.51, SCOPUS ID：51749102869
• A security engineering environment based on ISO/IEC standards: Providing standard, formal, and consistent supports for design, development, operation, and maintenance of secure information systems　　　　　　　　　　　　　　　
  Jingde Cheng; Yuichi Goto; Shoichi Morimoto; Daisuke Horie
  PROCEEDINGS OF THE SECOND INTERNATIONAL CONFERENCE ON INFORMATION SECURITY AND ASSURANCE, First page：350, Last page：+, 2008, [Reviewed]
  An intrinsic difficulty in ensuring security of information systems is that assailants (crackers) are active persons who can get knowledge and skills day after day and then continuously attack target information systems always with new techniques. Therefore, designers, developers, users, and maintainers of information systems with high security requirements need continuous supports for their tasks to protect the systems from assailants. However, until now, there is no systematic methodology proposed for this purpose. Based on our consideration that the continuous supports for system designers, developers, users, and maintainers only can be provided by a standard, formal, and consistent methodology, this paper proposes the new concept of security engineering environment and presents a real security engineering environment we are developing based on ISO/IEC information security standards in order to provide designers, developers, users, and maintainers with standard, formal, and consistent supports for design, development, operation, and maintenance of information systems with high security requirements.
  IEEE COMPUTER SOC, English, International conference proceedings
  DOI：https://doi.org/10.1109/ISA.2008.106
  DOI ID：10.1109/ISA.2008.106, Web of Science ID：WOS:000256051100067
• Fast qualitative reasoning about actions for computing anticipatory systems　　　　　　　　　　　　　　　
  Natsumi Kitajima; Yuichi Goto; Jingde Cheng
  ARES 2008: PROCEEDINGS OF THE THIRD INTERNATIONAL CONFERENCE ON AVAILABILITY, SECURITY AND RELIABILITY, First page：171, Last page：178, 2008, [Reviewed]
  A computing anticipatory system has to reason about actions as fast as possible in order to decide its next actions anticipatorily. We have implemented an action reasoning engine with general-purpose for various computing anticipatory systems and performed some experiments with the action reasoning engine and empirical knowledge represented quantitatively. Our experiments showed that the quantitative approach is very time-consuming and therefore it is not suitable to computing anticipatory systems with high reliability and high security requirements. This paper presents a qualitative approach for reasoning about actions fast. We show that the qualitative approach is more effective than the quantitative approach and therefore it is more suitable to computing anticipatory systems with high reliability and high security requirements.
  IEEE COMPUTER SOC, English, International conference proceedings
  DOI：https://doi.org/10.1109/ARES.2008.118
  DOI ID：10.1109/ARES.2008.118, Web of Science ID：WOS:000256665200024
• ISEDS: An information security engineering database system based on ISO standards　　　　　　　　　　　　　　　
  Daisuke Horie; Shoichi Morimoto; Noor Azimah; Yuichi Goto; Jingde Cheng
  ARES 2008: PROCEEDINGS OF THE THIRD INTERNATIONAL CONFERENCE ON AVAILABILITY, SECURITY AND RELIABILITY, First page：1219, Last page：+, 2008, [Reviewed]
  Security facilities of information systems with high securiry requirements should be consistently and continuously developed, used, and maintained based on some common standards of information security. However there is no engineering environment that can support all tasks in security engineering consistently and continuously. To construct a security engineering environment, a database that can manage all data concerning all tasks in security engineering is indispensable. This paper presents an Information Security Engineering Database System, named "ISEDS," that we are developing based on ISO standards, and shows its some possible applications. ISEDS manages data of ISO standards of information security and various cases of system development and maintenance. We adopted the international standard ISO/IEC 15408 (Common Criteria) for information security evaluation as one of ISO standards to underlie ISEDS, and implemented major functions of ISEDS and its application tools to manage and use data of ISO/IEC 15408. Developers, users, and maintainers can create, correct, and verify specification documents of security facilities with the application tools.
  IEEE COMPUTER SOC, English, International conference proceedings
  DOI：https://doi.org/10.1109/ARES.2008.76
  DOI ID：10.1109/ARES.2008.76, Web of Science ID：WOS:000256665200171
• Classification, formalization and verification of security functional requirements　　　　　　　　　　　　　　　
  Shoichi Morimoto; Shinjiro Shigematsu; Yuichi Goto; Jingde Cheng
  SOFSEM 2008: THEORY AND PRACTICE OF COMPUTER SCIENCE, Volume：4910, First page：622, Last page：+, 2008, [Reviewed]
  This paper proposes a new hybrid method to formally verify whether the security specification of a target information system satisfies security functional requirements defined in ISO/IEC 15408 evaluation criteria for security. We classify at first the security functional requirements of ISO/IEC 15408 into two classes: static requirements concerning static properties and dynamic requirements concerning dynamic behavior of target systems, and then formalize the static requirements with Z notation and the dynamic requirements with temporal logic. Thus, we can verify static properties using theorem-proving and dynamic behavior using model-checking. As a result, developers can easily use the method to verify whether the security specification of a target information system satisfies both static and dynamic security functional requirements defined in ISO/IEC 15408. The new method is an evolution and improvement of our early verification method where only Z notation was adapted and to verify dynamic behavior of target systems is difficult.
  SPRINGER-VERLAG BERLIN, English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-540-77566-9
  DOI ID：10.1007/978-3-540-77566-9, ISSN：0302-9743, Web of Science ID：WOS:000253521400054
• Development and Applications of ISEDS: An Information Security Engineering Database System　　　　　　　　　　　　　　　
  HORIE DAISUKE; MORIMOTO SHOICHI; GOTO YUICHI; CHENG JINGDE
  IPSJ journal, Volume：48, Number：8, First page：2684, Last page：2698, Aug. 2007, [Reviewed]
  Security facilities of information systems with high security requirements have to be designed, implemented, used, and maintained consistently and continuously. However, there was no tool that can support all activities in designing, developing, and maintaining security facilities of information systems consistently and continuously. This paper presents the development and applications of ISEDS, an Information Security Engineering Database System we are developing. ISEDS manages data about information security criteria, data about cases of development and maintenance of security facilities, and data denned by its various users. Developers, users, and maintainers of information systems can retrieve and update these data and also easily generate, correct and verify specifications about security facilities with additional tools of ISEDS. We adopted the international standard ISO/IEC 15408 for information security evaluation as one of security criteria that ISEDS deals with, and implemented functions of ISEDS and its additional tools to manage and use data related to ISO/IEC 15408.
  Information Processing Society of Japan (IPSJ), Japanese, Scientific journal
  ISSN：1882-7764, CiNii Articles ID：110006386498, CiNii Books ID：AN00116647
• Distributed Hash Table Based Design of Soft System Buses　　　　　　　　　　　　　　　
  Mohammad Reza Selim; Takumi Endo; Yuichi Goto; Jingde Cheng
  Jun. 2007, [Reviewed]
  近年の情報社会において、稼働しつづけることができる、そして、時間の経過につれて進化することができる大規模計算システムへの要求が高まっている。ソフトシステムバス（SSB）はそのような計算システムを支援するためのミドルウェアプラットフォームとして提案された。本論文では、大規模P2Pシステムのための分散ハッシュテーブルプロトコルの一つであるChordに基づくSSBの設計を紹介する。我々の設計は、拡張性、こしょうからの自動回復、データの保存そして漸増的かつリアルタイムでの更新可能性および保守可能性などのSSBの要求を満たしている。また、SSBの要求の観点から我々の設計の評価を合わせて紹介する。
  English, International conference proceedings
• A Quantitative Analysis of Implicational Paradoxes in Classical Mathematical Logic　　　　　　　　　　　　　　　
  Yuichi Goto; Jingde Cheng
  Electronic Notes in Theoretical Computer Science, Volume：169, First page：87, Last page：97, Mar. 2007, [Reviewed]
  Classical mathematical logic includes a lot of "implicational paradoxes" as its logic theorems. This paper uses the property of strong relevance as the criterion to identify implicational paradoxes in logical theorems of classical mathematical logic, and enumerates logical theorem schemata of classical mathematical logic that do not satisfy the strong relevance. This quantitative analysis shows that classical mathematical logic is by far not a suitable logical basis for automated forward deduction. © 2007 Elsevier B.V. All rights reserved.
  English, Scientific journal
  DOI：https://doi.org/10.1016/j.entcs.2006.07.031
  DOI ID：10.1016/j.entcs.2006.07.031, ISSN：1571-0661, SCOPUS ID：33847136724
• ENQUETE-BAISE: A general-purpose E-questionnaire server for ubiquitous questionnaire　　　　　　　　　　　　　　　
  Jingde Cheng; Yuichi Goto; Masato Koide; Keigo Nagahama; Masami Someya; Yusuke Utsumi; Ayaka Shionoiri
  2ND IEEE ASIA-PACIFIC SERVICES COMPUTING CONFERENCE, PROCEEDINGS, First page：187, Last page：+, 2007, [Reviewed]
  Questionnaire is a general and indispensable method frequently and widely used in many academic, engineering, medical, commercial, and political survey research activities to obtain systematic data and information. Ubiquitous questionnaire, i.e., to provide users with E-questionnaire services anytime and anywhere such that one can use E-questionnaire servers without even thinking about them, is an ideal ubiquitous service in service-oriented computing. Until now, there is no E-questionnaire server that is generally accepted and widely used. This paper presents a general-purpose E-questionnaire server we are developing for ubiquitous questionnaire, named "ENQUETE-BAISE," that can be used as a ready-made E-questionnaire server component in various web service systems as well as an alone E-questionnaire server with general-purpose for various questionnaires. ENQUETE-BAISE can also be used as an E-voting server with general-purpose by restricting its general functions and strengthening its security functions. The paper proposes the notion of ubiquitous questionnaire, presents a requirement analysis for ubiquitous questionnaire servers, introduces in brief persistent computing systems which are indispensable to implementation of ubiquitous questionnaire servers, and presents the architecture and facilities of ENQUETE-BAISE.
  IEEE COMPUTER SOC, English, International conference proceedings
  DOI：https://doi.org/10.1109/APSCC.2007.73
  DOI ID：10.1109/APSCC.2007.73, Web of Science ID：WOS:000254380500026
• Measuring reactability of persistent computing systems　　　　　　　　　　　　　　　
  Takumi Endo; Yuichi Goto; Jingde Cheng
  SOFTWARE COMPOSITION, Volume：4829, First page：144, Last page：151, 2007, [Reviewed]
  A persistent computing system is a reactive system that functions continuously anytime without stopping its reactions even when it needs to be maintained, upgraded, or reconfigured, it has some trouble, or it is attacked. However, the requirement that a computing system should run continuously and persistently is never taken into account as an essential and/or general requirement by traditional system design and development methodologies. As a result, there is no clearly defined standard to be used for measuring the reactability of a computing system. This paper proposes the first method to measure the reactability of a persistent computing system in a unified way. The paper introduces the notion of reactive processing path among components and shows that the reactive processing paths can be used to measure the reactability of a persistent computing system.
  SPRINGER-VERLAG BERLIN, English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-540-77351-1
  DOI ID：10.1007/978-3-540-77351-1, ISSN：0302-9743, Web of Science ID：WOS:000253263700011
• A replication oriented approach to event based middleware over structured peer to peer networks　　　　　　　　　　　　　　　
  Mohammad Reza Selim; Yuichi Goto; Jingde Cheng
  Proceedings of the 5th International Workshop on Middleware for Pervasive and Ad-hoc Computing, MPAC 2007 held at the ACM/IFIP/USENIX 8th International Middleware Conference, First page：61, Last page：66, 2007, [Reviewed]
  Due to efficient event dissemination and mobility support, event based middlewares are gaining popularity in pervasive computing environments. However, loss of events caused by broker/client failures or unreliable network connections is a common problem in existing event based middlewares. Middlewares providing support to critical distributed systems must be reliable enough not to lose published events. In this paper, we present the design of REM, a large scale Replication based type and attribute oriented Event Middleware over structured peer to peer (p2p) network. REM safeguards event losses by replicating the states of a broker in the neighboring overlay nodes. REM provides lossless mobility support to the clients even in a highly dynamic environment. Copyright 2007 ACM.
  English, International conference proceedings
  DOI：https://doi.org/10.1145/1376866.1376877
  DOI ID：10.1145/1376866.1376877, SCOPUS ID：57349111747
• A cooperative grid computing approach to automated theorem finding and automated problem proposing　　　　　　　　　　　　　　　
  Jingde Cheng; Yuichi Goto; Shinsuke Nara; Takahiro Koh
  KNOWLEDGE-BASED INTELLIGENT INFORMATION AND ENGINEERING SYSTEMS: KES 2007 - WIRN 2007, PT II, PROCEEDINGS, Volume：4693, First page：840, Last page：851, 2007, [Reviewed]
  This paper proposes a novel research direction: to build the Theory Grid as cooperatively shared formal theories within a virtual organization, and then to implement a crowd of automated reasoning programs working based on the Theory Grid such that as the wisdom of crowds a grid theorist has the ability to find new theorems and propose new questions automatically or semi-automatically. The paper also presents an architecture of the Theory Grid and,grid theorists, and major scientific challenges and technical issues in the implementation of the Theory Grid and grid theorists.
  SPRINGER-VERLAG BERLIN, English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-540-74827-4
  DOI ID：10.1007/978-3-540-74827-4, ISSN：0302-9743, Web of Science ID：WOS:000250338600106
• FreeEnCal: A forward reasoning engine with general-purpose　　　　　　　　　　　　　　　
  Jingde Cheng; Shinsuke Nara; Yuichi Goto
  KNOWLEDGE-BASED INTELLIGENT INFORMATION AND ENGINEERING SYSTEMS: KES 2007 - WIRN 2007, PT II, PROCEEDINGS, Volume：4693, First page：444, Last page：452, 2007, [Reviewed]
  A forward reasoning engine is an indispensable component in many advanced knowledge-based systems with purposes of creation, discovery, or prediction. This paper presents a forward reasoning engine with general-purpose, named "FreeEnCal", which can interpret and perform inference rules defined and given by its users, draw fragments of various classical and/or non-classical logic systems formalized as different formal systems, draw empirical theorems of various formal theories constructed based on various logic systems, and perform deductive, inductive, and abductive reasoning automatically. FreeEnCal can be used as a ready-made forward reasoning engine serving as a core and fundamental component in various advanced knowledge-based systems as well as an alone forward reasoning engine with general-purpose. The paper presents our basic ideas to design and implement FreeEnCal, facilities provided by FreeEnCal, and some applications of FreeEnCal.
  SPRINGER-VERLAG BERLIN, English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-540-74827-4
  DOI ID：10.1007/978-3-540-74827-4, ISSN：0302-9743, Web of Science ID：WOS:000250338600056
• EPLAS: An epistemic programming language for all scientists　　　　　　　　　　　　　　　
  Isao Takahashi; Shinsuke Nara; Yuichi Goto; Jingde Cheng
  COMPUTATIONAL SCIENCE - ICCS 2007, PT 1, PROCEEDINGS, Volume：4487, First page：406, Last page：+, 2007, [Reviewed]
  Epistemic Programming has been proposed as a new programming paradigm for scientists to program their epistemic processes in scientific discovery. As the first step to construct an epistemic programming environment, this paper proposes the first epistemic programming language, named 'EPLAS'. The paper analyzes the requirements of an epistemic programming language, presents the ideas to design EPLAS, shows the important features of EPLAS, and presents an interpreter implementation of EPLAS.
  SPRINGER-VERLAG BERLIN, English, International conference proceedings
  DOI：https://doi.org/10.1007/978-3-540-72584-8
  DOI ID：10.1007/978-3-540-72584-8, ISSN：0302-9743, Web of Science ID：WOS:000247062800052
• Formal Verification of Security Specifications with Common Criteria　　　　　　　　　　　　　　　
  Shoichi Morimoto; Shinjiro Shigematsu; Yuichi Goto; Jingde Cheng
  APPLIED COMPUTING 2007, VOL 1 AND 2, First page：1506, Last page：+, 2007, [Reviewed]
  This paper proposes a formalization and verification technique for security specifications, based on common criteria. Generally, it is difficult to define reliable security properties that should be applied to validate an information system. Therefore, we have applied security functional requirements that are defined in the ISO/IEC 15408 common criteria to the formal verification of security specifications. We formalized the security criteria of ISO/IEC 15408 and developed a pro cess, using Z notation, for verifying security specifications. We also demonstrate some examples of the verification instances using the theorem prover Z/EVES. In the verification process, one can verify strictly whether specifications satisfy the security criteria defined in ISO/IEC 15408.
  ASSOC COMPUTING MACHINERY, English, International conference proceedings
  DOI：https://doi.org/10.1145/1244002.1244325
  DOI ID：10.1145/1244002.1244325, Web of Science ID：WOS:000268215700289
• 動的再構成の観点からのソフトシステムバスとエンタープライズサービスバスの比較　　　　　　　　　　　　　　　
  染谷雅美; MohammadRezaSelim; 後藤祐一; 程京徳
  Volume：2007, Number：2, First page：77, Last page：78, Jan. 2007, [Reviewed]
  ソフトシステムバスを，エンタープライズサービスバス技術を用いて実現できるかを明らかにするために，構築されたシステムの動的再構成の観点からソフトシ
  
  ステムバスとエンタープライズサービスバスの比較を行う．
  Japanese, Symposium
• An Anticipatory Reasoning Engine for Anticipatory Reasoning-Reacting Systems
  NARA S.
  International Journal of Computing Anticipatory Systems, CHAOS, Volume：18, First page：225, Last page：234, Dec. 2006, [Reviewed]
  先行推論反応システムのもっとも重要なコンポーネントは、先行推論エンジン（ARE）である。本論文では、AREの要求とAREのプロトタイプを紹介する。始めに、先行推論について説明し、次に要求分析、機能の設計をおこなう。そして、実装上の課題について議論し、我々の実装の工夫について紹介する。最後に、現在の実験結果を紹介する。また、どのように先行推論版王システムがAREから有効な予測を得るかについて議論する。
  English, Scientific journal
  CiNii Articles ID：10020790279
• 情報セキュリティ工学データベースシステムISEDSの開発と応用　　　　　　　　　　　　　　　
  堀江大輔; 森本祥一; 後藤祐一; 程京徳
  First page：59, Last page：60, Oct. 2006, [Reviewed]
  Japanese, Symposium
• ISO/IEC 15408 に基づく定理証明とモデル検査による情報セキュリティ仕様の検証技法　　　　　　　　　　　　　　　
  森本祥一; 重松真二郎; 後藤祐一; 程京徳
  Volume：23, Number：3, First page：117, Last page：133, Jul. 2006, [Reviewed]
  情報システムの設計・開発において，セキュリティ仕様とその検証は重要な課題となっている．検証を行うには基準が必要であるが，情報システムが備えるべきセキュリティの基準を定めることは難しい．このため本論文では，IT製品や情報システムのセキュリティ評価の国際標準である ISO/IEC15408 を基準として採用し，これに基づいた情報セキュリティ仕様の形式手法による検証技法を提案する．本検証技法では，形式的に記述した ISO/IEC15408 のセキュリティ評価基準を用いて，対象となる情報システムの仕様が ISO/IEC15408 の基準を満たしているかどうかを定理証明とモデル検査により厳密に検証することができる．
  Japanese, Scientific journal
• A Security Specification Verification Technique Based on the International Standard ISO/IEC 15408　　　　　　　　　　　　　　　
  Shoichi Morimoto; Shinjiro Shigematsu; Yuichi Goto; Jingde Cheng
  First page：1802, Last page：1803, Apr. 2006, [Reviewed]
  English, International conference proceedings
  DOI：https://doi.org/10.1145/1141277.1141701
  DOI ID：10.1145/1141277.1141701
• A Quantitative Analysis of Implicational Paradoxes in Classical Mathematical Logic　　　　　　　　　　　　　　　
  Yuichi Goto; Jingde Cheng
  First page：42, Last page：43, Apr. 2006, [Reviewed]
  English, International conference proceedings
  DOI：https://doi.org/10.1145/1141277.1141286
  DOI ID：10.1145/1141277.1141286
• The theory grid and grid theorists　　　　　　　　　　　　　　　
  Jingde Cheng; Shinsuke Nara; Takahiro Koh; Yuichi Goto
  2006 2nd International Conference on Semantics Knowledge and Grid, SKG, First page：32, 2006, [Reviewed]
  This paper proposes a novel research direction: to build the Theory Grid as cooperatively shared formal theories within a virtual organization, and then to implement Grid Theorists as the wisdom of crowds working based on the Theory Grid such that the grid theorists have the ability to find new theorems and propose new questions semi-automatically. © 2006 IEEE.
  English, International conference proceedings
  DOI：https://doi.org/10.1109/SKG.2006.104
  DOI ID：10.1109/SKG.2006.104, SCOPUS ID：44949178748
• Comparative study between soft system bus and traditional middlewares　　　　　　　　　　　　　　　
  Mohammad Reza Selim; Takumi Endo; Yuichi Goto; Jingde Cheng
  ON THE MOVE TO MEANINGFUL INTERNET SYSTEMS 2006: OTM 2006 WORKSHOPS, PT 2, PROCEEDINGS, Volume：4278, First page：1264, Last page：+, 2006, [Reviewed]
  Although persistent availability is one of the basic requirements of the middlewares for pervasive computing systems to provide "anytime anywhere" services, very little work has been done on this issue. Soft System Bus (SSB) was proposed to provide "anytime anywhere" middleware platform support to large-scale reactive systems which run continuously and persistently. However, till now no SSB has been implemented. In this paper, we present a comparative study between the SSB and different types of traditional middlewares, e.g., synchronous Request/Reply, Message Oriented, Publish/ Subscribe middlewares, etc, in order to find the implementation issues of an SSB. We show that although existing middlewares have some characteristics that are common in an SSB too, they lack some features which are unique and essential for an SSB. Finally, we present the implementation issues of an SSB to ensure persistent availability.
  SPRINGER-VERLAG BERLIN, English, International conference proceedings
  DOI：https://doi.org/10.1007/11915072
  DOI ID：10.1007/11915072, ISSN：0302-9743, Web of Science ID：WOS:000243321400030
• Persistent computing systems as an infrastructure for pervasive services　　　　　　　　　　　　　　　
  Jingde Cheng; Yuichi Goto; Masami Someya; Takumi Endo
  2006 1ST INTERNATIONAL SYMPOSIUM ON PERVASIVE COMPUTING AND APPLICATIONS, PROCEEDINGS, First page：104, Last page：+, 2006, [Reviewed]
  Both pervasive (ubiquitous) computing and service-oriented computing implicitly require computing systems functioning anytime available throughout the physical world. However, the requirement that a computing system should run continuously and persistently is never taken into account as an essential and/or general requirement by traditional system design and development methodologies. As a result, a traditional computing system often has to stop its running and service when it needs to be maintained, upgraded, or reconfigured, it has some trouble, or it is attacked. This is not desirable to any pervasive (ubiquitous) service. This paper intends to propose a systematic and methodological solution to the problem: to develop persistent computing systems with soft system bus technology to provide an infrastructure for various pervasive services. After introducing the notions of persistent computing system and-soft system bus, we present two case studies of web service systems to show why persistent computing systems based on soft system buses are useful to pervasive services, and discuss benefits and challenges of our approach.
  IEEE, English, International conference proceedings
  DOI：https://doi.org/10.1109/SPCA.2006.297551
  DOI ID：10.1109/SPCA.2006.297551, Web of Science ID：WOS:000240859900019
• A prototype implementation of an anticipatory reasoning-reacting system　　　　　　　　　　　　　　　
  Feng Shang; Shinsuke Nara; Takashi Omi; Yuichi Goto; Jingde Cheng
  Computing Anticipatory Systems, Volume：839, First page：401, Last page：414, 2006, [Reviewed]
  This paper presents the first prototype of anticipatory reasoning-reacting system (ARRS). First, we briefly analyze implementation issues of an ARRS, present our considerations on the implementation of the first prototype, and implementation issues under these considerations; second, we introduce the architecture of the prototype system we implemented, the important components, the problems we met and solutions adopted in these components; and then, we present a case study to show and discuss some primitive experimental results on the prototype system; finally, we briefly compare our prototype system with several other computing anticipatory systems from the viewpoints of basic approaches and application fields.
  AMER INST PHYSICS, English, International conference proceedings
  DOI：https://doi.org/10.1063/1.2216650
  DOI ID：10.1063/1.2216650, ISSN：0094-243X, Web of Science ID：WOS:000238647800031
• ユビキタスサービスのための汎用電子アンケートサーバ ENQUETE-BAISE　　　　　　　　　　　　　　　
  染谷雅美; 内海悠輔; 塩野入彩香; 後藤祐一; 程京徳
  Volume：2006, Number：2, First page：41, Last page：42, Jan. 2006, [Reviewed]
  Japanese, Symposium
• Webアプリケーションシステムにおけるパフォーマンスボトルネックの分類と考察　　　　　　　　　　　　　　　
  通拉ガ; 染谷雅美; 後藤祐一; 程京徳
  Volume：2006, Number：2, First page：39, Last page：40, Jan. 2006, [Reviewed]
  Japanese, Symposium
• 人の集まりを支援するツールQWikS（クウィックス）　　　　　　　　　　　　　　　
  後藤祐一; 遠藤匠; 染谷雅美; 高橋勲男; 程京徳
  First page：175, Last page：176, Jan. 2006, [Reviewed]
  近年，WWWを介してのコミュニケーションが可能になってきている．掲示板やチャット，ICQ，メッセンジャー，SNS（Social Networking Site），Weblogなどのツールを使い，見知らぬ人同士がWWWを介してコミュニティを構成するようにった．また，グループウェアが普及し，会社内や同一部署内でスケジュールや資料を共有し，仕事を円滑に進めることができるようになった．しかしながら，Web上で構成したコミュニティや，地域活動，会社，学校などで構成したコミュニティの構成メンバーが集おうとするときには，日取りの調整や場所の選定など幹事に負担のかかる仕事が生じてしまう．本研究では，人が集まるときの不便を考察し，人が集まることを支援するツールQWikSを提案する．
  
  Japanese, Symposium
• ISO/IEC 15408 に基づく定理証明とモデル検査による情報セキュリティ仕様の検証技法　　　　　　　　　　　　　　　
  森本祥一; 重松真二郎; 後藤祐一; 程京徳
  First page：12, Last page：13, Oct. 2005, [Reviewed]
  Japanese, Symposium
  CiNii Articles ID：10017630867
• 並列化による前向き演繹エンジンの高速化　　　　　　　　　　　　　　　
  奈良信介; 後藤祐一; 程京徳
  Volume：46SIG10 (TOM12), Number：10, First page：19, Last page：29, Jul. 2005, [Reviewed]
  推論とは，既知の事実や仮説を前提とし，新しい結論を導出する過程である．現在，定理発見システムや先行予測システムなど様々な分野の情報システムで，与えられた前提から新しい結論を導出できる推論エンジンが求められている．実用的な推論エンジンを実現する際の最大の課題は効率である．なぜなら，推論エンジンは，妥当な結論を導出する為に，膨大な数の中間生成物を処理しなければならず，本質的に非効率な処理となってしまう為である．本研究では効率的な推論エンジンを実現する為に，推論の一つの方法である前向き演繹の並列計算モデルを提案する．また，そのモデルに基づいて推論エンジンの一種である汎用前向き自動帰結演算システムEnCal の実装を PC クラスタ上で行い，その有効性を実証する．
  Japanese, Scientific journal
  ISSN：0387-5806, CiNii Articles ID：10016425288
• Security Issues in Persistently Reactive Systems　　　　　　　　　　　　　　　
  Takumi Endo; Junichi Miura; Koichi Nanashima; Shoichi Morimoto; Yuichi Goto; Jingde Cheng
  First page：56, Last page：57, Jun. 2005, [Reviewed]
  English
• 永続コンピューティング環境を実現するソフトシステムバスパッケージの基本要求と機能　　　　　　　　　　　　　　　
  遠藤匠; 三浦潤一; 七島功一; 森本祥一; 後藤祐一; 程京徳
  Volume：2005, Number：5, First page：209, Last page：210, May 2005, [Reviewed]
  Japanese, Symposium
• Tasking Deadlocks in Programs with the Full Ada 95　　　　　　　　　　　　　　　
  Yasushi Tojo; Shinsuke Nara; Yuichi Goto; Jingde Cheng
  Volume：251, First page：48, Last page：56, Mar. 2005, [Reviewed]
  この論文では、Ada 95 リアルタイムシステム付属書に定義されているタスク同期待ち関係に関連するタスキングデッドロックのいくつかの例を紹介している。
  English, Scientific journal
  DOI：https://doi.org/10.1145/1064303.1064305
  DOI ID：10.1145/1064303.1064305
• Security in persistently reactive systems　　　　　　　　　　　　　　　
  T Endo; J Miura; K Nanashima; S Morimoto; Y Goto; JD Cheng
  EMBEDDED AND UBIQUITOUS COMPUTING - EUC 2005 WORKSHOPS, PROCEEDINGS, Volume：3823, First page：874, Last page：883, 2005, [Reviewed]
  From the viewpoints of dependable computing and ubiquitous computing, a new type of reactive systems, named Persistently Reactive Systems, was proposed. Persistently reactive systems cause some new security issues because of their continuous and persistent running without stopping their services. Based on the recognition that a persistently reactive systems can be constructed following the methodology of soft system buses, this paper defines security issues in persistently reactive systems with security requirements and security functions. To solve the issues, we propose a framework of SSB-connector, such that designers and developers can easily design and develop reliable and secure functional components of a persistently reactive system.
  SPRINGER-VERLAG BERLIN, English, Scientific journal
  DOI：https://doi.org/10.1007/11596042
  DOI ID：10.1007/11596042, ISSN：0302-9743, Web of Science ID：WOS:000235802200090
• General-purpose forward deduction engine for modal logics　　　　　　　　　　　　　　　
  S Nara; T Omi; Y Goto; JD Cheng
  KNOWLEDGE-BASED INTELLIGENT INFORMATION AND ENGINEERING SYSTEMS, PT 2, PROCEEDINGS, Volume：3682, First page：739, Last page：745, 2005, [Reviewed]
  Many advanced knowledge-based systems with purposes of discovery and/or prediction, such as anticipatory reasoning-reacting systems, legal reasoning systems, geographical information system, and so on, require a forward deduction engine for modal logics as an important component. However, until now, there is no forward deduction engine with the general-purpose for modal logics. This paper presents a general-purpose forward deduction engine for modal logics. We show some essential requirements and functions for a general-purpose forward deduction engine for modal logics, present our implementation of the forward deduction engine, and show possible applications based on our forward deduction engine.
  SPRINGER-VERLAG BERLIN, English, Scientific journal
  DOI：https://doi.org/10.1007/11552451
  DOI ID：10.1007/11552451, ISSN：0302-9743, Web of Science ID：WOS:000232722200101
• Efficient Anticipatory Reasoning for Anticipatory Systems with Requirements of High Reliability and High Security
  GOTO Y.
  International Journal of Computing Anticipatory Systems, Volume：14, First page：156, Last page：171, Dec. 2004, [Reviewed]
  高い信頼性と安全性が要求される実用的な先行システムは、その応用からくる要求を満たすために、許容できる時間内に十分な量の効果的な結論を先行的に得るための予測推論を行うことができなければならない。先行推論の実行時間は導出する結論の増加にともなって長くなるため、許容できる時間内に十分な量の結論を得るという要求は相反する。我々は、汎用帰結演算のための自動演繹エンジンEnCalを開発している。EnCalは、汎用帰結演算のための自動演繹エンジンであるが、我々は、時間相関論理に基づく先行推論を実行する先行システムの前向き演繹エンジンとしてEnCalが使えるのではないかと期待している。そのゴールを達成するための重要課題は、EnCalの効率性である。本論文では、並列処理技術によるEnCalの効率性の改善に案する実験とその結果について報告する。
  English, Scientific journal
  CiNii Articles ID：10016425291
• Representing and reasoning about spatial knowledge based on spatial relevant logic　　　　　　　　　　　　　　　
  JD Cheng; Y Goto
  CONCEPTUAL MODELING FOR ADVANCED APPLICATION DOMAINS, PROCEEDINGS, Volume：3289, First page：114, Last page：126, 2004, [Reviewed]
  Almost all existing methodologies for representing and reasoning about spatial knowledge are somehow based on classical mathematical logic or its various conservative extensions. This approach, however, may be suitable to searching and describing a formal proof of a previously specified statement, under the condition that we have complete and consistent knowledge., but not necessarily suitable to forming a new concept and discovering a new statement, in particular, in the case that our knowledge is incomplete and inconsistent. This paper proposes a new approach: representing and reasoning about spatial knowledge based on spatial relevant logic.
  SPRINGER-VERLAG BERLIN, English, Scientific journal
  DOI：https://doi.org/10.1007/b101694
  DOI ID：10.1007/b101694, ISSN：0302-9743, Web of Science ID：WOS:000225684500010
• ENQUETE-BAISE: ユビキタスアンケートのための汎用電子アンケートサーバ　　　　　　　　　　　　　　　
  後藤祐一; 小出雅人; 長濱圭吾; 程京徳
  Volume：2004, First page：81, Last page：84, Jan. 2004, [Reviewed]
  従来の紙ベースのアンケートでいつでも・どこでも・だれでも実施・回答できるアンケートを安全に実施しようとすると多大な金銭的・時間的コストが必要となる． 一方で，インターネット，計算機，携帯電話・端末などを利用した電子アンケートであれば，紙ベースのアンケートと比較して，低コストでいつでも・どこでも・だれでも実施・回答できるアンケートを安全に実施することができる．本論文では，いつでも・どこでも・だれでも安全に回答・実施を行なえるユビキタスアンケートという観点から，紙ベースのアンケートと電子アンケートを比較し，その違いを明らかにする．また，低コストでいつでも・どこでも・だれでもアンケートを安全に実施することのできる環境を提供するツールとして，われわれが開発し，一般公開している汎用電子アンケートサーバENQEUTE-BAISEを紹介する．
  Japanese, Symposium
  CiNii Articles ID：40006284776
• ソフトシステムバスの実現について -- ユビキタスコンピューティングのための永続システムを目指して　　　　　　　　　　　　　　　
  七島功一; 後藤祐一; 程京徳
  Volume：2004, First page：77, Last page：80, Jan. 2004, [Reviewed]
  ユビキタスコンピューティング環境の究極の目標は，いつでもどこでも利用可能な計算環境を提供することである．したがって，ユビキタスコンピューティングの前提として，いつでも利用可能な情報システムが必要となる．しかし，保守や更新などを行う時でさえ止まらずに動作し続けるシステムの実現には未だ至っていない．止まらずに動作し続けるシステムを実現するための基盤技術として，我々が提案したソフトシステムバスというソフトウェア機構が有用である．本論文では，まず，ソフトシステムバスの概念を紹介し，次に，それに対する要求とそれが提供すべき機能を列挙し，そして，ソフトシステムバスのもっとも重要な機能である指令・データの伝達と保存を基地局によって実現するモデルを提案する．
  Japanese, Symposium
  CiNii Articles ID：40006284775
• 並列化による推論エンジンの効率化　　　　　　　　　　　　　　　
  奈良信介; 後藤祐一; 程京徳
  First page：101, Last page：108, Oct. 2003, [Reviewed]
  Japanese
• Efficient Forward Deduction for Discovery and Prediction by Parallel Processing　　　　　　　　　　　　　　　
  Shinsuke Nara; Yuichi Goto; Jingde Cheng
  First page：76, Last page：82, Sep. 2003, [Reviewed]
  発見や予測のための自動前向き演繹エンジンは、許容される時間内に妥当な結論を得なければならない。なぜならば、妥当な結論を得られない、あるいは許容時間内に処理できないシステムは実用的な応用には使えないからである。しかし、どのような前向き演繹のプロセスは本質的に非効率なプロセスである。なぜならば、多くの中間生成物を扱わなければならないためである。よって、より多くの量の実行時間や主記憶領域が自動前向き演繹の実行に必要とされる。この問題は、どのような自動前向き演繹エンジンにおいても一般的である。本論文では、並列処理によって自動前向き演繹の効率を改善する。我々は、自動前向き演繹のための並列計算モデルを提案し、そのモデルに基づき、PCクラスタにおいて汎用帰結演算のための自動前向き演繹システムを実装する。
  English, International conference proceedings
• A Comparative Study on Paradoxical Conditionals in Classical Mathematical Logic, Relevant Logics, and Strong Relevant Logics　　　　　　　　　　　　　　　
  Yuichi Goto; Takahiro Koh; Jingde Cheng
  First page：69, Last page：75, Sep. 2003, [Reviewed]
  論理の観点から、我々は、古典数理論理、その伝統的拡張、そして、従来の相関論理が発見のための前向き推論や演繹を基礎づけるには適していないことを定性的に示した。なぜならば、それらの論理定理には実質含意のパラドクスが多く含まれているためである。そして、強相関論理が発見のための前向き推論や演繹を基礎づける論理体系としてより期待できる候補であることを示した。しかし、古典数理論理とその拡張、従来の相関論理がどのくらい悪いのか、また、強相関論理がどのくらい良いのかは、まだ定量的な分析と議論がおこなわれていないため、まだ明らかにされていない。本論文では、比較研究として強相関論理と古典数理論理に含まれる実質含意のパラドクスについて定量的な分析と議論を行う。この研究成果は、実質含意のパラドクスの量が、現実世界の応用のために役立つ前向き推論および演繹エンジンの開発にとって、とても重要であることを示している。
  English, International conference proceedings
• A Digital Reference Room for E-learning　　　　　　　　　　　　　　　
  Ru Lu; Feng Shang; Yuichi Goto; Jingde Cheng
  First page：17, Last page：21, Sep. 2003, [Reviewed]
  This paper addresses Digital Reference Room (DRR) for e-learning, a project that deals with two hot fields of studies for both IT industry and academic institution: digital library and e-learning. Our basic design ideas are to develop a user-friendly digital reference room utilizing a simple but effective architecture, taking advantage of XML and making efficient use of available open source offering. Hence, we adopted native XML database technology instead of traditional RDBMS (Relational Database Management Systems), and Apache's open source offering, Xindice as tools to develop the DRR. This paper describes the architecture and implementation of the digital reference room system for e-learning.
  English, International conference proceedings
• Automated Theorem Finding by Forward Deduction Based on Strong Relevant Logic: A Case Study in NBG Set Theory　　　　　　　　　　　　　　　
  Xiaobin Wang; Yuichi Goto; Shinsuke Nara; Jingde Cheng
  First page：83, Last page：91, Sep. 2003, [Reviewed]
  自動定理発見は、1988年にWosによって提案された自動推論に関する33の研究問題一つである。我々は、強相関論理を数学知識の表現と推論に用いて、かつ、強相関論理に基づく前向き演繹により定理の発見行うという自動定理発見問題へのアプローチを提案した。しかし、今のところ、このアプローチが本当に自動定理発見問題の解決にどのくらい有効かは明確ではない。本論文では、強相関論理に基づく自動前向き演繹によって、von Neumann-Vernays-Godel集合論（NBG集合論）における定理発見のための事例研究を紹介する。この事例研究によって、強相関論理は、定理発見に適していることが明らかになった。なぜならば、強相関論理に基づく自動前向き演繹によって導出されたNBG集合論の定理は、妥当であり、矛盾する定理は導出されなかったためである。
  English, International conference proceedings
• HILBERT : An Autonomous Evolutionary Information System for Teaching and Learning Logic　　　　　　　　　　　　　　　
  Jingde Cheng; Naoki Akimoto; Yuichi Goto; Masato Koide; Kouichi Nanashima; Shinsuke Nara
  First page：245, Last page：254, Jul. 2003, [Reviewed]
  論理の学習・教授のための広く有用なコンピューターに基づく環境を確立するために、我々は、自律的に進化する情報システムHILBERTを開発している。HILBERTは、科学的発見と同じく日々の論理的思考のための多様な論理形式を基礎づける様々な論理体系を学習・教授するためのものである。本論文では、HILBERTの基本設計アイデア、機能、サービス、そして、アーキテクチャを紹介する。
  English, International conference proceedings
• Parallel Forward Deduction System for General-Purpose Entailment Calculus on Clusters of PCs　　　　　　　　　　　　　　　
  Sinsuke Nara; Yuichi Goto; Daisuke Takahashi; Jingde Cheng
  First page：359, Last page：364, Oct. 2002, [Reviewed]
  帰結演算のための自動前向き演繹システムは、定理発見や知識発見システムのような前向き推論エンジンを必要とする多くの応用システムにおいて欠かすことのできないコンポーネントである。自動前向きシステムの性能は、その応用において非常に重要である。本論文では、PCクラスタにおいて、汎用帰結演算のための並列前向き演繹システムを提案する。また、提案したアルゴリズムの有効性と効率性を明らかにするために、アルゴリズムを実装したものの評価を行う。
  English, International conference proceedings
• Improving Performance of Automated Forward Deduction System EnCal? on Shared-Memory Paralell Computers　　　　　　　　　　　　　　　
  Yuichi Goto; Daisuke Takahashi; Jingde Cheng
  First page：63, Last page：68, Sep. 2002, [Reviewed]
  自動前向き演繹システムの性能は、その応用において非常に重要である。発見のために用いる前向き演繹システムには、あらかじめゴールとして特定の命題や定理を明示的にあたえられないため、前向き演繹システムはしばしば多くの冗長な中間生成物（既に導出されたもののと同じも）を導出する。よって、いかなる前向き演繹システムにおいても、どのように冗長な中間生成物を減らすかは、一般的かつ難しい課題である。本論文では、汎用帰結演算のための自動前向き演繹システムEnCalの性能を改善するために、冗長な中間生成物を発見する新しいアルゴリズムを提案する。また、そのアルゴリズムを共有メモリ型並列計算機上で動くEnCalに組み込み、提案アルゴリズムの有効性を実証する。
  English, International conference proceedings
• A strong relevant logic approach to the calculus of fuzzy conditionals　　　　　　　　　　　　　　　
  JD Cheng; Y Goto
  COMPUTATIONAL INTELLIGENT SYSTEMS FOR APPLIED RESEARCH, First page：66, Last page：74, 2002, [Reviewed]
  In order to obtain new fuzzy conditionals from known or assumed fuzzy propositions and fuzzy conditionals, a new approach to the calculus of fuzzy conditionals is proposed. The approach adopts strong relevant logic as the fundamental logic to underlie the calculus of fuzzy conditionals and performs the calculus using EnCal, an automated forward deduction system for general-purpose entailment calculus.
  WORLD SCIENTIFIC PUBL CO PTE LTD, English, International conference proceedings
  Web of Science ID：WOS:000186233300009
• 電子投票・アンケートはe-サービスになれるか　　　　　　　　　　　　　　　
  後藤祐一; 劉欣; 小出雅人; 高橋大介; 程京徳
  Volume：20022, Number：2, First page：63, Last page：64, Jan. 2002, [Reviewed]
  Japanese, Symposium
• システムバスを用いた反応的システムの構築法　　　　　　　　　　　　　　　
  七島功一; 後藤祐一; 程京徳
  Volume：20022, Number：2, First page：15, Last page：16, Jan. 2002, [Reviewed]
  Japanese, Symposium
• Parallel Forward Deduction Algorithms of General-Purpose Entailment Calculus on Shared-Memory Parallel Computers　　　　　　　　　　　　　　　
  Yuichi Goto; Daisuke Takahashi; Jingde Cheng
  First page：168, Last page：175, Aug. 2001, [Reviewed]
  帰結演算のための自動前向きシステムは、自律的推論エンジンを必要とするシステムたとえば、定理発見、動的データベース、知識発見システムのような多くの応用システムにとって欠くことのできないコンポーネントである。それらの応用にとって、自動前向き演繹システムの性能は、非常に重要である。本論文では、共用メモリ型並列計算機における汎用帰結演算のための並列前向き演繹アルゴリズムを提案している。また、そのアルゴリズムが効果的および効率的であるかどうかの評価を行っている。
  English, International conference proceedings

• アバタを活用してZoom Fatigueを軽減するオンライン会議システムの開発　　　　　　　　　　　　　　　
  高橋 拓未; 後藤 祐一
  Volume：2025, Number：1, First page：201, Last page：202, Mar. 2025, [Corresponding]
  Japanese, Summary national conference
• 転倒事故防止のためのリアルタイム歩道路面情報通知システム　　　　　　　　　　　　　　　
  金田 彩孝; 後藤 祐一
  Volume：2025, Number：1, First page：307, Last page：308, Mar. 2025, [Corresponding]
  Japanese, Summary national conference
• プレゼンスを用いた不安を生じさせる環境の段階的再現を行えるVR 曝露療法システムの開発　　　　　　　　　　　　　　　
  木本 翔太; 後藤 祐一
  Volume：2025, Number：1, First page：445, Last page：446, Mar. 2025, [Corresponding]
  Japanese, Summary national conference
• Improvement of Bicycle Helmet Detection Model Based on YOLOv9　　　　　　　　　　　　　　　
  Ruipeng Xu; Yuichi Goto
  Volume：2025, Number：1, First page：885, Last page：886, Mar. 2025, [Corresponding]
  English, Summary national conference
• A Case Study to Detection DDoS Attacks Using a Support Vector Machine Integrated with Random Forest in SDN Network　　　　　　　　　　　　　　　
  Yuqi Li; Yuichi Goto
  First page：183, Last page：184, Sep. 2024, [Corresponding]
  English, Summary national conference
• 前向き推論を用いた自動定理発見の試行支援環境の開発　　　　　　　　　　　　　　　
  山鹿 親作; 後藤 祐一
  Volume：2024, Number：1, First page：267, Last page：268, Mar. 2024, [Corresponding]
  Japanese, Summary national conference
• 演繹定理を用いた論理定理の推論規則化による強相関論理に基づく前向き推論を用いた自動定理発見法の改善　　　　　　　　　　　　　　　
  長谷川 諒; 後藤 祐一
  Volume：2024, Number：1, First page：269, Last page：270, Mar. 2024, [Corresponding]
  Japanese, Summary national conference
• 汎用前向き推論エンジンFreeEnCal?の簡潔データ構造SuRFを用いた省メモリ化　　　　　　　　　　　　　　　
  辻 陽成; 後藤 祐一
  Volume：2024, Number：1, First page：775, Last page：776, Mar. 2024, [Corresponding]
  Japanese, Summary national conference
• マルチコアCPUに対応した汎用前向き推論エンジンFreeEnCalの開発　　　　　　　　　　　　　　　
  多賀 靖晃; 後藤 祐一
  Volume：2024, Number：1, First page：785, Last page：786, Mar. 2024, [Corresponding]
  Japanese, Summary national conference
• リモート環境下でのタブレット端末を用いた電子試験における不正行為の検出および防止　　　　　　　　　　　　　　　
  久木田陽生; 後藤祐一
  Volume：2024, Number：1, First page：1015, Last page：1016, Mar. 2024, [Corresponding]
  Japanese, Summary national conference
• タブレットを用いたオフライン電子試験環境の構築　　　　　　　　　　　　　　　
  伍 嘉俊; 小河原 悠暉; 後藤 祐一
  Volume：2024, Number：1, First page：1017, Last page：1018, Mar. 2024, [Corresponding]
  Japanese, Summary national conference
• 不安への対処方法の段階的練習を行えるVR暴露療法システムのユーザビリティの向上　　　　　　　　　　　　　　　
  木本 翔太; 後藤 祐一
  Volume：2023-AAC-22, Number：1, First page：1, Last page：6, Jul. 2023, [Corresponding]
  Japanese, Summary national conference
• 棋譜と対応付けした将棋用語オントロジの構築　　　　　　　　　　　　　　　
  柳沢 健太; 後藤 祐一
  Volume：2023, Number：1, First page：135, Last page：136, Mar. 2023, [Corresponding]
  Japanese, Summary national conference
• 認識プログラミング言語EPLASの改善　　　　　　　　　　　　　　　
  相馬亮太; 後藤祐一; 三浦隆太; 奥山龍一
  Volume：2023, Number：1, First page：515, Last page：516, Mar. 2023, [Corresponding]
  Japanese, Summary national conference
• Construction of a Multimodal Japanese Tourism Knowledge Graph　　　　　　　　　　　　　　　
  Lina Feng; Yuichi Goto
  Volume：2023, Number：1, First page：523, Last page：524, Mar. 2023, [Corresponding]
  Japanese, Summary national conference
• YOLOv4 を用いた省メモリなマスク着用検出システム　　　　　　　　　　　　　　　
  覃 文標; 後藤 祐一
  Volume：2022, Number：1, First page：585, Last page：586, Mar. 2022, [Corresponding]
  Japanese, Summary national conference
• 不安を生じさせる環境の段階的再現および各段階での滞在支援を行えるVR暴露療法システムの開発　　　　　　　　　　　　　　　
  久野 亮; 後藤 祐一
  Volume：2022, Number：1, First page：899, Last page：900, Mar. 2022, [Corresponding]
  Japanese, Summary national conference
• 電子調査仕様記述言語のための構造化エディタ QSL Editor　　　　　　　　　　　　　　　
  阿曼吐爾; 熱吾漢; 後藤 祐一
  Volume：2021, Number：1, First page：271, Last page：272, Mar. 2021, [Corresponding]
  Japanese, Summary national conference
• 強相関論理に基づく前向き推論を用いた自動定理発見法の項書き換え処理による改善　　　　　　　　　　　　　　　
  高島 望; 後藤 祐一
  Volume：2021, Number：1, First page：477, Last page：478, Mar. 2021, [Corresponding]
  Japanese, Summary national conference
• DNS増幅攻撃検出システムのためのSVMカーネル関数の比較　　　　　　　　　　　　　　　
  李 陽; 後藤 祐一
  Volume：2021, Number：1, First page：447, Last page：448, Mar. 2021, [Corresponding]
  Japanese, Summary national conference
• 不安に対する対処方法の段階的な練習を追加したVR暴露療法システムの開発　　　　　　　　　　　　　　　
  久野 亮; 後藤 祐一
  Volume：2021, Number：1, First page：811, Last page：812, Mar. 2021, [Corresponding]
  Japanese, Summary national conference
• A Case Study of Formal Analysis Methods with Reasoning for Cryptographic Protocols　　　　　　　　　　　　　　　
  Jun Zheng; Yuichi Goto
  First page：123, Last page：126, Sep. 2020, [Corresponding]
  English, Summary national conference
• Linked Data を用いた理論グリッドの構築 -- 公理的集合論の形式理論フラグメントを用いた事例研究　　　　　　　　　　　　　　　
  佐久間 亜都武; 後藤 祐一; 高 宏彪; 程 京徳
  Volume：2018, Number：1, First page：463, Last page：464, Mar. 2018, [Corresponding]
  自動定理発見は計算機に定理を自動的に証明させるのではなく、計算機に未知の定理を自動的に発見させることである。自動定理発見のためのインフラストラクチャとして理論グリッドおよびその理論的基礎が提案された。理論グリッドはさまざまな論理体系に基づく、さまざまな形式理論の部分集合を組織化し、管理する環境である。しかし、理論グリッドは未だ構築されていない。本研究ではデータをWeb上で相互にリンク付けして公開できる仕組みであるLinked Dataを用いた理論グリッドの構築法を提案した。また、公理的集合論の形式理論の部分集合を格納する理論グリッドのプロトタイプを構築した。
  Japanese, Summary national conference
• 前向き推論エンジンを用いた自動非単調推論 -- デフォルト論理における事例研究　　　　　　　　　　　　　　　
  伊藤 拓也; 後藤 祐一; 程 京徳
  Volume：2018, Number：1, First page：91, Last page：92, Mar. 2018
  前向き推論エンジンは、前提として与えられた論理式群および推論の結果得られた論理式群に推論規則を適用し、終了条件を満たすまで論理式を導出するプログラムである。汎用前向き推論エンジンFreeEnCalは、推論エンジンの一種であり、これまで自動単調推論を実現する用途で利用されてきた。しかし、自動非単調推論への応用はまだ行われていない。本研究では、前向き推論エンジンを用いた自動非単調推論機構の実現の第一歩として、非単調推論の一つであるデフォルト論理に基づく推論においてFreeEnCalを用いた自動推論機構を提案し、その有用性を検討する。
  Japanese, Summary national conference
• A Formal Analysis Method with Reasoning for Key Exchange Protocols　　　　　　　　　　　　　　　
  我妻 和憲; 後藤 祐一; 程 京徳
  IPSJ Journal, Volume：56, Number：3, First page：903, Last page：910, 15 Mar. 2015
  Formal analysis of cryptographic protocols is used to find flaws before using the protocols. In traditional formal analysis method with proving such as model checking and theorem proving, analysts must enumerate flaws before analysis when they verify that a cryptographic protocol has not those flaws. In other words, those methods can detect only flaws that analysts enumerate. An idea of formal analysis to use forward reasoning to detect flaws of cryptographic protocols was proposed and logic systems underlying forward reasoning were presented. However, its concrete method is not established. This paper presents a concrete method of formal analysis with reasoning for key exchange protocols and shows its effectiveness. By the proposed method, we analyzed a key exchange protocol and detect flaws that analysts did not enumerate in traditional formal analysis method with proving. Therefore, the proposed method is effective for detecting flaws that analysts overlooked. Finally, we discussed that the proposed method can be extended to various cryptographic protocols.
  Information Processing Society of Japan (IPSJ), Japanese
  ISSN：1882-7764, CiNii Articles ID：110009884083, CiNii Books ID：AN00116647
• Development of a Tasking Deadlock Detector for Ada 2012 Programs　　　　　　　　　　　　　　　
  驛場 猛雄; 後藤 祐一; 程 京徳
  Volume：6, Number：2, First page：105, Last page：105, 29 Aug. 2013
  プログラミング言語Adaは高信頼性の求められる組込みシステム開発のための並行型プログラミング言語である．Adaプログラムにおいて，タスクの同期待ちによるデッドロック（タスキングデッドロック）が発生しうる．Ada 95以前のバージョンでは，タスキングデッドロックの完全な識別方法が提案されており，また，その動的検出ツールが開発されている．一方，Ada 2005およびAda 2012においては，新たな同期待ち処理の追加により，Adaプログラム中に新たな種類のタスキングデッドロックが発生する可能性があるが，まだそれについての報告はされていない．さらに，Ada 2005およびAda 2012で新たに導入された機能や文法が存在するため，Ada 95プログラムのためのタスキングデッドロック動的検出ツールはAda 2012プログラムでは利用することができない．本発表では，Ada 2012プログラムで新たに生じうるタスキングデッドロックについての調査結果を報告する．そして，Ada 2012プログラムに対応したタスキングデッドロックの動的検出ツールの実現とその有用性を示す．Ada is a concurrent programming language for programming high reliable embedded systems. A method to completely identify tasking deadlocks in Ada 95 programs was proposed, and, a tasking deadlock detector, to detect tasking deadlocks in Ada 95 programs at run-time, was also developed. The tasking deadlock detector for Ada 95 programs cannot be used for Ada 2012 programs because Ada 2012 has several changes from Ada 95 from viewpoint of syntax or facility. However, no tasking deadlock detector for Ada 2012 programs has been developed. This presentation presents a tasking deadlock detector for Ada 2012 programs, and shows its effectiveness.
  Japanese
  ISSN：1882-7802, CiNii Articles ID：110009602865, CiNii Books ID：AA11464814
• セキュリティターゲットの作成と保守を支援するツールST-Editorの開発　　　　　　　　　　　　　　　
  三浦潤一; 後藤祐一; 程京徳
  Volume：2013, Number：7, First page：1, Last page：8, 20 May 2013
  情報セキュリティの観点から，情報システム・製品が適切に設計され，その設計が正しく実装されていることを評価するための国際標準規格として，ISO/IEC15408（Common Criteria，CC） が策定され利用されている．CC の認証を取得するためには，情報システムのセキュリティ設計仕様書であるセキュリティターゲット （Security Target，ST） を作成しなければならない．一方で，毎日のように，情報システム・製品に対する新たな脆弱性や，攻撃方法が発見されており，脆弱性の修正や対策機能の追加のために情報システム・製品の保守作業が必要不可欠である．その際には，情報システム・製品そのものの保守作業だけでなく，セキュリティ設計仕様書である ST の保守作業もあわせて行う必要がある．しかし，ST の作成・保守作業は，人的・金銭的・時間的コストがかかり，人為的ミスも発生しやすいため，ST の作成・保守作業を支援するためのツールが必要とされている．本研究では，ST の作成と保守を支援するツール ST-Editor を開発した．ST-Editor は，ST の構造を視覚的に表示し，その構造をもとに ST の作成や編集が行える．また，ST の作成において，難しい点，時間のかかる点，ミスを起こしやすい点を支援する機能を備えており，ST-Editor を利用することで，ST 作成・保守時の労力の軽減，ミスの低減が期待できる．
  Japanese
  ISSN：0919-6072, CiNii Articles ID：110009579847, CiNii Books ID：AA12149313
• セキュリティターゲットの作成と保守を支援するツールST-Editorの開発　　　　　　　　　　　　　　　
  三浦潤一; 後藤祐一; 程京徳
  Volume：2013, Number：7, First page：1, Last page：8, 20 May 2013
  情報セキュリティの観点から，情報システム・製品が適切に設計され，その設計が正しく実装されていることを評価するための国際標準規格として，ISO/IEC15408（Common Criteria，CC） が策定され利用されている．CC の認証を取得するためには，情報システムのセキュリティ設計仕様書であるセキュリティターゲット （Security Target，ST） を作成しなければならない．一方で，毎日のように，情報システム・製品に対する新たな脆弱性や，攻撃方法が発見されており，脆弱性の修正や対策機能の追加のために情報システム・製品の保守作業が必要不可欠である．その際には，情報システム・製品そのものの保守作業だけでなく，セキュリティ設計仕様書である ST の保守作業もあわせて行う必要がある．しかし，ST の作成・保守作業は，人的・金銭的・時間的コストがかかり，人為的ミスも発生しやすいため，ST の作成・保守作業を支援するためのツールが必要とされている．本研究では，ST の作成と保守を支援するツール ST-Editor を開発した．ST-Editor は，ST の構造を視覚的に表示し，その構造をもとに ST の作成や編集が行える．また，ST の作成において，難しい点，時間のかかる点，ミスを起こしやすい点を支援する機能を備えており，ST-Editor を利用することで，ST 作成・保守時の労力の軽減，ミスの低減が期待できる．
  Japanese
  CiNii Articles ID：110009579625, CiNii Books ID：AN10112981
• 汎用的な自動定理発見ツールの実現と応用　　　　　　　　　　　　　　　
  後藤祐一
  Volume：第6号(平成19年度), Sep. 2008
  Japanese, Report research institution
• D-023 Implementation and Applications of an Application program Interface for Information Security Engineering Database System : ISEDS　　　　　　　　　　　　　　　
  Horie Daisuke; Goto Yuichi; Cheng Jingde
  Volume：6, Number：2, First page：53, Last page：56, 22 Aug. 2007
  Forum on Information Technology, Japanese
  CiNii Articles ID：110007688414, CiNii Books ID：AA11740605
• ユビキタスコンピューティングの基盤としての永続コンピューティング(研究成果報告)　　　　　　　　　　　　　　　
  後藤祐一
  Volume：40, First page：67, Last page：69, 2007
  Japanese, Report research institution
• Persistent Computing Systems as an Infrastructure of Ubiquitous Computing
  後藤祐一
  Volume：39, First page：133, Last page：134, Jul. 2006
  This research report presents some current results of our research project "Persistent Computing Systems as an Infrastructure of Ubiquitous Computing" supported in part by Saitama University
  Japanese, Report research institution
  ISSN：1880-4446, CiNii Articles ID：120001370442
• 追加機能を含んだAda 95プログラムのためのタスキングデッドロック検出ツール　　　　　　　　　　　　　　　
  藤乘靖士; 奈良信介; 後藤祐一; 程京徳
  Volume：46, Number：14, Jan. 2005
  Ada 95並行プログラムにおけるタスキングデッドロックとは, 同期待ち関係により閉路が作られることでプログラムの実行ができなくなる状態である.そしてAda 95で作られたプログラムを対象としたタスキングデッドロック検出法が開発され実装が行われている.この検出法はTask-Wait-For Graphを構成しタスキングデッドロック検出の条件を調べることで検出を行う.しかし, この検出法は標準部分と追加機能で構成されるAda 95の標準部分のみを使用したプログラムしか対象としていないため, 追加機能を使用したプログラムの場合には検出が行えない.本発表では追加機能を含んだAda95プログラムのためのタスキングデッドロック検出ツールの開発を行った.タスキングデッドロックの要因である同期待ち関係を追加機能部分について調べ, 従来と別の種類の同期待ち関係が存在することが分かった.そこで従来のTask-Wait-For Graphをプログラムが追加機能を含んだ場合にも利用できるように拡張を行った.タスキングデッドロックの検出条件についても拡張を行い, 新たな種類のタスキングデッドロックの検出も行えるようにした.このように拡張・修正したAda 95プログラム向けのタスキングデッドロック検出法に基づき, 検出ツールの実装を行った.そして実際にツールを使ったタスキングデッドロックの検出例を示した.
  ISSN：0387-5806, CiNii Articles ID：110002769916

• Apr. 2020 - Present
  Mathmatical Logic, Saitama University, 命題論理、述語論理、推論、導出原理 を扱っている。, Undergraduate special subjects
• Apr. 2019 - Present
  Theory of Programming Languages, Saitama University, プログラミング言語とは何か、形式的意味論とは何か、具体構文と抽象構文、構造帰納法、操作意味論、評価意味論、計算意味論、プログラミング言語の主要構成成分の形式的意味論に関する基礎知識について講義する。, Undergraduate special subjects
• Apr. 2018 - Present
  Advanced Information Processing, Tokyo University of Science, システム構築において広く利用されているリレーショナルデータベース (RDB) について学ぶ。また、非リレーショナルデータベースの一例として、知識グラフなどで利用されているグラフデータベースを紹介する。, Undergraduate special subjects
• 2017 - Present
  Exercise on Practical System Development, Saitama University, チームで、スマートフォンアプリケーションなどを用いたビジネスサービスの企画から実現まで行う。また、開発の過程で頻繁に発表を実施する。そのフィードバックを活かして、サービス開発を改良することを経験する。また、最後にサービスの発表会を行う。, Undergraduate special subjects
• Apr. 2015 - Present
  Advanced Lectures on Knowledge Representation, Saitama University, 知識表現として、ホーン節、オブジェクト指向、意味ネットワーク、記述論理、非単調推論を扱う。, Postgraduate courses
• Apr. 2011 - Present
  Computer Literacy, Saitama University, Unix／Linuxの基本的な使い方および、Unix／Linux上においてレポート作成方法を実際にコマンドを手を動かしつつ学ぶ。, Undergraduate special subjects
• 2017 - 2024
  Practical System Development II, Saitama University, 秋学期に開講されるプロジェクト・ベースド・ラーニング(PBL)科目である『実践的システム開発演習』の準備のためにチーム開発とスマートフォンアプリケーション開発の基礎を学ぶ集中講義。, Undergraduate special subjects
• 2017 - 2024
  Practical System Development I, Saitama University, 秋学期に開講されるプロジェクト・ベースド・ラーニング(PBL)科目である『実践的システム開発演習』の準備のためにチーム開発とスマートフォンアプリケーション開発の基礎を学ぶ集中講義。, Undergraduate special subjects
• Apr. 2016 - Mar. 2020
  情報倫理
• Apr. 2016 - Mar. 2019
  Natural Language Processing, Saitama University, Faculty of Engineering, Department of Information and Computer Sciences
• Apr. 2015 - Mar. 2019
  コンピュータネットワーク
• Apr. 2008 - Mar. 2016
  離散数学演習
• Apr. 2005 - Mar. 2009
  計算論演習

• 2018 - Present
• 2016 - Present, THE INSTITUTE OF ELECTRONICS, INFORMATION AND COMMUNICATION ENGINEERS
• 2005 - Present, Association for Computing Machinery
• 2005 - Present, IEEE-CS
• 2003 - Present, THE JAPANESE SOCIETY FOR ARTIFICIAL INTELLIGENCE
• 2001 - Present, INFORMATION PROCESSING SOCIETY OF JAPAN

• Implementation and Applications of Anticipatory Reasoning-Reacting Systems　　　　　　　　　　　　　　　
  Ministry of Education, Culture, Sports, Science and Technology, Grants-in-Aid for Scientific Research(基盤研究(B)), 基盤研究(B), 2006 - 2009
  Jingde CHENG; Yuichi GOTO, 埼玉大学, Coinvestigator not use grants
  Grant amount(Total)：6120000, Direct funding：5400000, Indirect funding：720000
  Almost all existing reactive systems are passive from the viewpoint of reliability and security, because they can only perform the operations in response to external stimulus but have no ability to response to disasters and attacks, and deal with them actively. Anticipatory Reasoning-Reacting Systems was proposed as a new type of reactive system with high reliability and high security that detect and predict omens of attacks and failures anticipatorily, take some actions to inform its users, and perform some operations to defend attacks and failures by themselves. In this research, we have ...
  Competitive research funding, Grant number：18300005
• An Automated Theorem Finding System for General-purpose and Its Applications　　　　　　　　　　　　　　　
  Ministry of Education, Culture, Sports, Science and Technology, Grants-in-Aid for Scientific Research(若手研究(B)), 若手研究(B), 2007 - 2008
  Yuichi GOTO, 埼玉大学, Principal investigator
  Grant amount(Total)：2780000, Direct funding：2300000, Indirect funding：480000
  Competitive research funding, Grant number：19700127