図面 (/)

技術 モデルチェッカーを用いた様相不動点論理体系による通信サービス分類方法

出願人 日本電信電話株式会社
発明者 楢崎修二堀田英一
出願日 1992年12月25日 (27年4ヶ月経過) 出願番号 1992-346288
公開日 1994年7月15日 (25年9ヶ月経過) 公開番号 1994-197170
状態 未査定
技術分野 交換機の特殊サービス (2) 中央制御交換方式 電話通信サービス
主要キーワード プロセス論理 並行プロセス モデルチェッカ サービス利用者間 並行プログラム 遷移規則 状態遷移機械 変化過程
関連する未来課題
重要な関連分野

この項目の情報は公開日時点(1994年7月15日)のものです。
また、この項目は機械的に抽出しているため、正しく解析できていない場合があります

図面 (7)

目的

利用者視点から見た通信サービス分類を可能にする。

構成

通信サービスの利用者の利用目的と考えられるサービス利用者の情報所有状態の変化過程形式的に記述することのできる様相不動点論理体系を用いて、該利用者が要求するサービスプログラム性質論理式表現する。実際の通信サービスを実現するプログラムを構成する各プロセスのとり得る状態、動作、遷移規則初期状態、記憶長を与えることにより該プログラムを有限状態遷移機械として決定する。与えられた有限状態遷移機械に対する構造が前記論理式を充足するかどうかを、論理体系の意味論にしたがい検証を行うモデルチェッカーを用いて検証し、利用者の視点から見た通信サービスの分類を可能にする。

概要

背景

通信サービス分類は、従来はその実現に要するハードウェア機能に着目して行なわれてきた。これは、ネットワークの持つ処理機能が必要に応じて付加されてきたという歴史背景に基づく分類基準である。この方法は、サービス提供側には妥当な分類基準であった。

しかし、通信サービスの種類や個数が増加すると、利用者の要求に対して、どのサービスが利用可能なのかを判断するのは、人手による困難な作業となる。また、既存サービスの組み合わせによる提供可能性を考えると一層の困難が生じる。

概要

利用者の視点から見た通信サービスの分類を可能にする。

通信サービスの利用者の利用目的と考えられるサービス利用者の情報所有状態の変化過程形式的に記述することのできる様相不動点論理体系を用いて、該利用者が要求するサービスプログラム性質論理式表現する。実際の通信サービスを実現するプログラムを構成する各プロセスのとり得る状態、動作、遷移規則初期状態、記憶長を与えることにより該プログラムを有限状態遷移機械として決定する。与えられた有限状態遷移機械に対する構造が前記論理式を充足するかどうかを、論理体系の意味論にしたがい検証を行うモデルチェッカーを用いて検証し、利用者の視点から見た通信サービスの分類を可能にする。

目的

今日の通信業界は、ネットワークの高速化・デジタル化情報処理能力の増大等の理由により、量・種類共に多くのサービスを提供するに至っている。そのため、上記の問題は解くべき重要性増している。

効果

実績

技術文献被引用数
0件
牽制数
1件

この技術が所属する分野

ライセンス契約や譲渡などの可能性がある特許掲載中! 開放特許随時追加・更新中 詳しくはこちら

請求項1

通信サービスとして記述された並行プログラム分類方法であって、該サービス利用者利用目的と考えられる、サービス利用者の情報所有状態の変化過程形式的に記述することのできる様相不動点論理体系を用いて、該利用者が要求するサービスプログラム性質論理式表現し、実際の通信サービスを実現するプログラムを構成する各プロセスのとり得る状態、動作、遷移規則初期状態、記憶長を与えることにより該プログラムを有限状態遷移機械として決定し、与えられた有限状態遷移機械に対する構造が前記論理式を充足するかどうかを、論理体系の意味論にしたがい検証を行うモデルチェッカーを用いて検証し、利用者の視点から見た通信サービスの分類を可能にする、モデルチェッカーを用いた様相不動点論理体系による通信サービス分類方法。

技術分野

0001

本発明は、電話ファックスパソコン通信等、情報交換の手段を提供することを目的とした通信サービスと呼ばれる並行プログラム分類方法に関する。

背景技術

0002

通信サービスの分類は、従来はその実現に要するハードウェア機能に着目して行なわれてきた。これは、ネットワークの持つ処理機能が必要に応じて付加されてきたという歴史背景に基づく分類基準である。この方法は、サービス提供側には妥当な分類基準であった。

0003

しかし、通信サービスの種類や個数が増加すると、利用者の要求に対して、どのサービスが利用可能なのかを判断するのは、人手による困難な作業となる。また、既存サービスの組み合わせによる提供可能性を考えると一層の困難が生じる。

発明が解決しようとする課題

0004

上述した従来技術の持つ問題点は、そのサービス分類方法を用いる場合には、そこにおいて分類基準として使われている「サービスを実現するのに必要なネットワークの持つ処理機能」とはどういうものなのかが、実際のシステムに依存したものとなり、一般的な抽象化がされていないということである。従って、ハードウェアから離れた視点に立つと、その分類基準の妥当性は明らかではなく、ハードウェアの詳細を知らないサービスの利用者と、その考案者や実現者等の間の意志疎通を妨げる原因となっている。

0005

今日の通信業界は、ネットワークの高速化・デジタル化情報処理能力の増大等の理由により、量・種類共に多くのサービスを提供するに至っている。そのため、上記の問題は解くべき重要性増している。

0006

まとめると、現在の問題は以下のようになる。

0007

・通信サービスに対する利用者の視点から見た分類方法の欠如
・その基盤となる形式要求記述法の欠如
したがって、この問題の解決には、サービスの利用者の視点から記述可能な形式的記述による、サービス・プログラムの分類・検証が必要である。

0008

現在、並行プログラムをはじめとするプログラムの性質を、ある論理体系上で意味を定められた論理式で形式的に記述し、また、性質を推論するというプログラムの仕様検証方法が既に提案されている。

0009

しかし、情報の伝達を目的とするという特殊な要求を持つ通信サービスに対する仕様検証技法としては、提案されている論理体系は不十分な記述力しかなく、情報の伝達という観点から記述される仕様の検証にはそぐわないという問題がある。

0010

本発明の目的は、利用者の視点からみた通信サービスの分類を行なう、通信サービスの分類方法を提供することにある。

課題を解決するための手段

0011

本発明の通信サービスの分類方法は、通信サービスの利用者の利用目的と考えられる、サービス利用者間の情報所有状態の変化過程を形式的に記述することのできる様相不動点論理体系を用いて、該利用者が要求するサービスプログラムの性質を論理式で表現し、実際の通信サービスを実現するプログラムを構成する各プロセスのとり得る状態、動作、遷移規則初期状態、記憶長を与えることにより該プログラムを有限状態遷移機械として決定し、与えられた有限状態遷移機械に対する構造が前記論理式を充足するかどうかを、論理体系の意味論にしたがい検証を行うモデルチェッカーを用いて検証し、利用者の視点から見た通信サービスの分類を可能にする。

0012

本発明は、(1)論理式を用いてユーザの要求の形式的な記述を可能にする、(2)利用者の要求を形式的に記述するために、並行プロセス上の知識所有状態に関する推論を行なう共通知識論理と、並行プロセスの動作に関する性質を記述するプロセス論理と、不動点演算子によって対象の性質を記述する不動点論理とを融合した様相論理体系を用いる、(3)論理体系を定めることにより、形式的に書かれた利用者要求に関する推論を可能にする、(4)与えられた利用者の要求が実際のサービスを有限状態遷移機械として書いたものの性質として成り立つかどうかをモデルチェッカーによって自動的に判定することにより、検証の機械化を行なうものである。

0013

モデルチェッカーとは、与えられたある構造上で、与えられた論理式が充足可能であるかどうかを、論理体系の意味論を用いて決定するプログラムである。

0014

通常の通信サービスを実現するプログラムの多くは、有限状態遷移機械と考えられる。プログラムを構成する各プロセスのとり得る状態、動作、遷移規則、初期状態、記憶長を与えることにより、プログラムの動作が有限状態遷移機械として決定できる。この有限状態遷移機械を構造とする。

0015

通信サービスに対する利用者の抽象的な要求を、知識の所有状態とプロセスの動作によって変化する状態を表すことのできる論理式で記述する。有限状態遷移機械に対応する構造上で論理式を規定する論理体系の意味を定めておくことにより、与えられた構造上で論理式が成立するかどうかを決定することができる。

0016

モデルチェッカーは、与えられた有限状態遷移機械に対応する構造が、与えられた論理式を充足するかどうかを論理体系の意味論に従い、検証する。モデルチェッカーはその論理式を充足するような性質を、与えられた有限状態遷移機械が持つ場合には「真」の値を返し、そうでない場合は「」の値を返す。このモデルチェッカーの出力を用いることにより、与えた論理式に対する通信サービスの検証が可能になる。

0017

また、種々の通信サービスに対して同等の式をモデルチェッカーに与えた時の出力結果(図1)により、通信サービスはその式を充足するものとしないものに二分することができる。この分類を繰り返し適用することにより、利用者の様々な視点から見た通信サービスの分類が可能になる。

0018

提案する分類方法では、サービスの実現に必要な機能は構造の中に暗黙的に記述され、利用者の要求を記述する論理式中には出現しないため、従来の分類方法の問題の解決策となっている。

0019

次に、本発明の実施例について図面を参照して説明する。

0020

通常の電話サービスとファックスの性質の差を本発明により記述・判定できることを以下に示す。

0021

図2は通常の電話サービスを有限状態遷移機械として記述したものである。

0022

処理の流れを簡単に述べる。送り手sは受け手プロセスに接続要求open_regを出す。受け手rは(1)接続可能な場合(OK)、(2)不在の場合、(3)話中の場合(busy)、に応じた処理を行なう。(1)の場合は回線の接続on_hook(r)を行ない、送り手sから情報を受け取る。(2)および(3)の場合は送り手s側により接続要求open_regが取り消され、両者とも初期状態reset(s),reset(r)に復帰する。受け手rが情報を獲得した場合はそれ以降の状態で原子命題が成立する(図斜線部)。従って、初期状態reset(r),reset(s)は、情報を受け取らなかった場合と、情報を受け取った場合の2つが存在する。送り手sにより情報の伝達は任意回繰り返すことができる。

0023

図3ファックスサービスを有限状態遷移機械として記述したものであり、図4はファックスで情報を受け取った後、正しく情報が伝わったならば受け手rが送り手sに確認の電話を入れるプロトコルのシステム(これを仮に受信通知ファックスと呼ぶことにする)を有限状態遷移機械として記述したものである。

0024

なお、図3図4中「send_fax」はファックスの送信であり、「send−fax」の次の「open_reg」はファックス受信確認であり、「ack」は「OK」に対する確認である。

0025

一方、利用者の要求を形式的に記述するための論理体系として以下のような様相演算子を持つ様相不動点論理体系を考える。これはプロセス論理として知られる様相論理体系(文献:Milner,R.:Communication and Concurrency,Prentice-Hall International,1985.)と、共通知識論理を呼ばれる論理体系(文献:Halpern,J.Y.:"Knowledge and Common Knowledge in a Distributed Environment",Journal of theACM,Vol.37,No.3,July 1990,pp.549-587.)、さらに不動点論理の融合である。

0026

ID=000003HE=005 WI=013 LX=1435 LY=1550
不動点変数Xを含む式φが成立する(通常、最小不動点と呼ばれるものである)。

0027

ID=000004HE=005 WI=011 LX=1445 LY=1800
動作aを行なった後では式φが成り立つ可能性がある。

0028

ID=000005HE=005 WI=011 LX=1445 LY=2000
動作aを行なった後では式φが常に成り立つ。

0029

ID=000006HE=005 WI=009 LX=1455 LY=2200
エージェントiは式φを知っている。

0030

不動点演算子μを使うことにより、以下のような様相演算子を簡便のために導入することができる。

0031

ID=000007HE=005 WI=011 LX=1445 LY=2550
任意の動作を任意有限回行なった後で式φが成り立つ可能性がある。

0032

ID=000008HE=005 WI=011 LX=0545 LY=0300
任意の動作を任意有限回行なった後で式φが必ず成り立つ。

0033

ID=000009HE=010 WI=009 LX=0555 LY=0550
グループgの全てのエージェントiにおいて

0034

ID=000010HE=005 WI=009 LX=1455 LY=0400
が成立する。

0035

このような論理体系における、利用者の要求の論理式による記述例は以下のようなものである。

0036

ID=000011HE=010 WI=118 LX=0460 LY=0700
(1)式中に出現する記号の説明をする。sは送り手を、rは受け手を示す。has(r,info)は原子命題であり、受け手rが情報infoを持っていることを示す。これより、上式はある動作は実行可能であり、その動作を行なった後では送り手sが受け手rが情報を受け取ったことを確認できることを表す式であることがわかる。

0037

この式をモデルチェッカーに与えることにより、真偽値を得ることができるが、この場合は真の値となる。

0038

同様の論理式を図3に示すファックス、図4に示す受信通話ファックスと共にモデルチェッカーに与え、真偽値を計算すると、ファックスでは「偽」の値が、受信通知ファックスでは「真」の値が得られる。

0039

この結果により、図5に示すように、通常の電話サービスと受信通知ファックスは与えた仕様、すなわち、送り手は受け手が情報を受信したことを確認できるかどうかという観点から同じ範疇に入ることがわかり、一方、ファックスはこの仕様を満たさないことがわかる。

0040

利用者の要求を記述する論理式の例としては他に以下のようなものが考えられる。

0041

ID=000012HE=010 WI=120 LX=0450 LY=1400
これを用いた通信サービスの仕様検証例として不在メッセージ電話(図6)を考える。この不在メッセージ電話は掛かってきた電話を受け取るべき人間がいない時に、代わりにメッセージを流すサービスである。この仕様は以下のように考えられる。
在席時には、不在状態に変更されるまで通常の電話サービスを実行する
・不在時に、在席状態に変更されるまで着呼した場合にはメッセージを流す
・特定の操作(ボタンを押す)が行なわれるまで、在席/不在モードが変更されない。
この仕様の中で、特に、ある操作が行なわれるまでは在席モード/不在モードが変更されず、何度でもモードで特定された機能を実行するという部分に対する仕様を上式は表している。また、(1)式が電話および不在メッセージ電話において成立することにより、この不在メッセージ電話は通常の電話サービスの拡張であることがわかる。

発明の効果

0042

以上説明したように本発明は、通信サービスの利用者の利用目的と考えられるサービス利用者の情報所有状態の変化過程を形式的に記述することのできる論理体系を用いてサービスプログラムの性質を表すことにより、通信サービスプログラムの性質を厳密に推論することができ、利用者の視点からみた通信サービスの検証や分類が可能になり、これにより、(1)利用者−サービス実現者間の厳密なサービスの仕様理解、(2)通信サービスの機械的な検証・分類、が可能になる効果がある。

図面の簡単な説明

0043

図1モデルチェッカーの入出力図である。
図2通常の電話サービスを有限状態遷移機械として記述した図である。
図3ファックスサービスを有限状態遷移機械として記述した図である。
図4受信通知ファックスを有限状態遷移機械として記述した図である。
図5電話、ファックス、受信通知ファックスの通信サービスに対して、式(1)の観点から行なったモデルチェッキングの結果得られたサービスの分類結果を示す図である。
図6不在メッセージ電話の状態遷移図である。

ページトップへ

この技術を出願した法人

この技術を発明した人物

ページトップへ

関連する挑戦したい社会課題

該当するデータがありません

関連する公募課題

該当するデータがありません

ページトップへ

おススメ サービス

おススメ astavisionコンテンツ

新着 最近 公開された関連が強い技術

  • TOTO株式会社の「 認知機能判定システム」が 公開されました。( 2020/02/13)

    【課題】 毎日確実に認知機能を判定すると共に、認知機能の異常を従来よりも精度良く判定することが可能な認知機能判定システムを提供することを目的とする。【解決手段】 トイレ室に設置された便器と、トイレ... 詳細

  • 株式会社日立製作所の「 避難誘導システム」が 公開されました。( 2020/02/13)

    【課題】災害発生時において、現在の避難所の状況を鑑みて、適切な避難先を避難者に提案することのできる、避難誘導システムを提供する。【解決手段】避難者に避難する避難所を提案する避難誘導システムであって、利... 詳細

  • 株式会社TKアジャイルの「 情報システム」が 公開されました。( 2020/02/13)

    【課題】従来の通信方法に比べ簡易で処理負荷の少ない情報システムを提供する。【解決手段】外部の装置3に対して入出力を行うとともに、インターネット5を介してデータを送受信するサーバ10と、インターネット5... 詳細

この 技術と関連性が強い技術

関連性が強い 技術一覧

この 技術と関連性が強い人物

関連性が強い人物一覧

この 技術と関連する社会課題

該当するデータがありません

この 技術と関連する公募課題

該当するデータがありません

astavision 新着記事

サイト情報について

本サービスは、国が公開している情報(公開特許公報、特許整理標準化データ等)を元に構成されています。出典元のデータには一部間違いやノイズがあり、情報の正確さについては保証致しかねます。また一時的に、各データの収録範囲や更新周期によって、一部の情報が正しく表示されないことがございます。当サイトの情報を元にした諸問題、不利益等について当方は何ら責任を負いかねることを予めご承知おきのほど宜しくお願い申し上げます。

主たる情報の出典

特許情報…特許整理標準化データ(XML編)、公開特許公報、特許公報、審決公報、Patent Map Guidance System データ