|
3
|
1 \documentclass[submit,techrep,noauthor]{ipsj}
|
|
|
2 %\documentclass{ipsj}
|
|
|
3
|
|
|
4 \usepackage[dvipdfmx]{graphicx}
|
|
|
5 \usepackage{latexsym}
|
|
|
6 \usepackage{listings}
|
|
5
|
7 \setcounter{year}{2021}
|
|
|
8
|
|
3
|
9
|
|
|
10 \def\Underline{\setbox0\hbox\bgroup\let\\\endUnderline}
|
|
|
11 \def\endUnderline{\vphantom{y}\egroup\smash{\underline{\box0}}\\}
|
|
|
12 \def\|{\verb|}
|
|
|
13
|
|
|
14 %\setcounter{巻数}{59}
|
|
|
15 %\setcounter{号数}{1}
|
|
|
16 %\setcounter{page}{1}
|
|
|
17 \pagestyle{empty}
|
|
|
18
|
|
|
19
|
|
|
20
|
|
|
21 %\受付{2016}{3}{4}
|
|
|
22 %\再受付{2015}{7}{16} %省略可能
|
|
|
23 %\再再受付{2015}{7}{20} %省略可能
|
|
|
24 %\再再受付{2015}{11}{20} %省略可能
|
|
|
25 %\採録{2016}{8}{1}
|
|
|
26
|
|
|
27
|
|
|
28
|
|
|
29
|
|
|
30 \begin{document}
|
|
4
|
31 \bibliographystyle{ipsjunsrt} % for bibliography
|
|
3
|
32
|
|
|
33
|
|
|
34 \title{Gears OSのモデル検査の実装}
|
|
|
35
|
|
|
36 \etitle{Implementing Gears OS Model Checking}
|
|
|
37
|
|
4
|
38 %\affiliate{IPSJ}{情報処理学会\\
|
|
|
39 %IPSJ, Chiyoda, Tokyo 101--0062, Japan}
|
|
3
|
40
|
|
|
41
|
|
4
|
42 \affiliate{IE}{琉球大学工学部\\
|
|
|
43 Faculty of Engineering, University of the Ryukyus}
|
|
3
|
44
|
|
|
45 \author{河野 真治}{Kono Shinji}{IE}[kono@ie.u-ryukyu.ac.jp]
|
|
|
46
|
|
|
47
|
|
|
48 \begin{abstract}
|
|
|
49 \input{abstract}
|
|
|
50 \end{abstract}
|
|
|
51
|
|
|
52
|
|
|
53 \begin{jkeyword}
|
|
|
54 モデル検査, OS
|
|
|
55 \end{jkeyword}
|
|
|
56
|
|
|
57 \begin{eabstract}
|
|
|
58 Gears OS has continuation based description of user programs and the kernel. Using meta programming facility, we can
|
|
|
59 perform model checks on the user program and even the kernel itself. In this paper, we show an implmentation on
|
|
|
60 the model checking and show the evalution.
|
|
|
61 \end{eabstract}
|
|
|
62
|
|
|
63 \begin{ekeyword}
|
|
|
64 Model checking, OS
|
|
|
65 \end{ekeyword}
|
|
|
66
|
|
|
67 \maketitle
|
|
|
68
|
|
|
69 \input 0.tex
|
|
|
70
|
|
|
71
|
|
4
|
72 \bibliography{ref}
|
|
3
|
73
|
|
|
74 \end{document}
|
