著者

Masaki NAKAMURA Shuki HIGASHI Kazutoshi SAKAKIBARA Kazuhiro OGATA

出版者

The Institute of Electronics, Information and Communication Engineers

雑誌

IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences (ISSN:09168508)

巻号頁・発行日

vol.E105-A, no.5, pp.823-832, 2022-05-01

被引用文献数

3

---

Because processes run concurrently in multitask systems, the size of the state space grows exponentially. Therefore, it is not straightforward to formally verify that such systems enjoy desired properties. Real-time constrains make the formal verification more challenging. In this paper, we propose the following to address the challenge: (1) a way to model multitask real-time systems as observational transition systems (OTSs), a kind of state transition systems, (2) a way to describe their specifications in CafeOBJ, an algebraic specification language, and (3) a way to verify that such systems enjoy desired properties based on such formal specifications by writing proof scores, proof plans, in CafeOBJ. As a case study, we model Fischer's protocol, a well-known real-time mutual exclusion protocol, as an OTS, describe its specification in CafeOBJ, and verify that the protocol enjoys the mutual exclusion property when an arbitrary number of processes participates in the protocol*.

著者

Atsushi Nishikawa Eiko Yoshinaga Masaki Nakamura Masayoshi Suzuki Keiji Kido Naoto Tsujimoto Taeko Ishii Daisuke Koide

出版者

Society for Clinical Epidemiology

雑誌

Annals of Clinical Epidemiology (ISSN:24344338)

巻号頁・発行日

vol.4, no.1, pp.20-31, 2022 (Released:2022-01-07)

参考文献数

21

被引用文献数

10

---

BACKGROUNDThis retrospective observational study validated case-finding algorithms for malignant tumors and serious infections in a Japanese administrative healthcare database.METHODSRandom samples of possible cases of each disease (January 2015–January 2018) from two hospitals participating in the Medical Data Vision Co., Ltd. (MDV) database were identified using combinations of ICD-10 diagnostic codes and other procedural/billing codes. For each disease, two physicians identified true cases among the random samples of possible cases by medical record review; a third physician made the final decision in cases where the two physicians disagreed. The accuracy of case-finding algorithms was assessed using positive predictive value (PPV) and sensitivity.RESULTSThere were 2,940 possible cases of malignant tumor; 180 were randomly selected and 108 were identified as true cases after medical record review. One case-finding algorithm gave a high PPV (64.1%) without substantial loss in sensitivity (90.7%) and included ICD-10 codes for malignancy and photographing/imaging. There were 3,559 possible cases of serious infection; 200 were randomly selected and 167 were identified as true cases after medical record review. Two case-finding algorithms gave a high PPV (85.6%) with no loss in sensitivity (100%). Both case-finding algorithms included the relevant diagnostic code and immunological infection test/other related test and, of these, one also included pathological diagnosis within 1 month of hospitalization.CONCLUSIONSThe case-finding algorithms in this study showed good PPV and sensitivity for identification of cases of malignant tumors and serious infections from an administrative healthcare database in Japan.

著者

二木 厚吉 緒方 和博 中村 正樹 Kokichi Futatsugi Kazuhiro Ogata Masaki Nakamura 北陸先端科学技術大学院大学情報科学研究科 北陸先端科学技術大学院大学情報科学研究科 北陸先端科学技術大学院大学情報科学研究科 Graduate School of Information Science Japan Advanced Institute of Science and Technology (JAIST) Graduate School of Information Science Japan Advanced Institute of Science and Technology (JAIST) Graduate School of Information Science Japan Advanced Institute of Science and Technology (JAIST)

出版者

日本ソフトウェア科学会

雑誌

コンピュータソフトウェア = Computer software (ISSN:02896540)

巻号頁・発行日

vol.25, no.2, pp.1-13, 2008-04-24

参考文献数

6

被引用文献数

3

---

CafeOBJ言語システムを用いた形式手法,すなわち形式仕様の作成法と検証法,を全6回にわたり解説する.CafeOBJ言語はOBJ言語を拡張した代数仕様言語であり,振舞仕様,書換仕様,パラメータ化仕様などが記述できる最先端の形式仕様言語である.CafeOBJ言語システムは,等式を書換規則として実行することで等式推論を健全にシミュレートすることができ,対話型検証システムとして利用出来る.第1回の今回は,「待ち行列を用いる相互排除プロトコル」を例題として,言語や検証法の細部に立ち入ることなく,CafeOBJ仕様の作成と検証が全体としてどのように行われるかを説明する.第2回以降では,言語の構文と意味(第2回),等式推論と項書換システム(第3回)について説明し,証明譜を用いた簡約のみに基づくCafeOBJの検証法(第4回)を解説する.さらに,認証プロトコル(第5回)と通信プロトコル(第6回)の2つの典型的な検証例も示すことで検証の技法についても解説する.The formal method, or the method for writing and verifying formal specifications, with the CafeOBJ language system is described in a series of six tutorials. The CafeOBJ language is a most advanced formal specification language which extents the OBJ language, and behavioral, rewriting, and parameterized specifications can be written in it. The CafeOBJ language system can simulate equational reasoning by executing equations as rewrite rules, and be used as an interactive verification system. This first tutorial presents an overview of the CafeOBJ formal method by using an example of "mutual exclusion protocol with a waiting queue" without getting into details of the language and the verification technique. In the following tutorials, the language and its semantics (2nd tutorial), equational reasoning and term rewriting systems (3rd tutorial) are presented, and the CafeOBJ's verification method with proof scores which only uses reductions (4th tutorial) is explained. Furthermore, CafeOBJ's verifications of an authentication protocol (5th tutorial) and a communication protocol (6th tutorial) are also presented, and several verification techniques are explained.