記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：ACM  

DOI： 10.1145/3651781.3651789

researchmap

その他リンク： https://dblp.uni-trier.de/rec/conf/icsca/2024

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：ACM  

For distributed systems in Functional Reactive Programming (FRP), we have been interested in glitch avoidance.
FRP describes systems by dataflow of time-varying values which are abstractions of values that change over time.
A glitch is a kind of inconsistencies between time-varying values due to update timing.
There are several researches for glitch avoidance and/or consistency of the values.
Since distributed systems often assume no global clocks nor locks, the existing methods send many messages to ensure one of these properties.
We propose a multi-party FRP language, named MPFRP.
In MPFRP, we describe some parties of time-varying values for the distributed system.
A party is a dataflow network whose time-varying values are updated consistently each other, but independently with those in other parties.
The concept of parties gives us a flexible scope for ensuring consistency and minimizing messages.

DOI： 10.1145/3631991.3632000

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：ACM  

This paper presents mechanisms for describing real-time tasks in functional reactive programming (FRP) languages for small-scale embedded systems. We have designed and implemented Emfrp, an FRP language for resource-constrained systems, and demonstrated its usefulness with several applications. However, the language requires using external clocks as time-varying values when describing time-dependent behaviors. In this work, we extend the types of time-varying values that express their update timings to describe periodic and aperiodic tasks. The extensions enable concise and precise descriptions of various timed behaviors. We evaluate prototype implementations of the extended languages concerning program size, execution time, and power consumption.

DOI： 10.1145/3623506.3623578

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

DOI： 10.1145/3594671.3594674

researchmap

その他リンク： https://dblp.uni-trier.de/db/conf/programming/programming2023.html#SuzukiWM23

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：ACM  

DOI： 10.1145/3563837.3568338

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）   出版者・発行元：Information Processing Sociey of Japan  

We introduce a new type system to Emfrp, a functional reactive programming (FRP) language designed for resource-constrained embedded systems. Functional reactive programming is a programming paradigm that allows concise descriptions of reactive systems such as GUIs by combining time-varying values that express values changing over time. Emfrp is a domain-specific language based on FRP, designed and developed for small-scale embedded systems. Because the language can statically determine the amount of runtime memory and guarantee the termination of reactive actions, a program written in Emfrp can safely continue reactive behaviors in resource-constrained environments. To ensure these properties, Emfrp disallows the use of recursive data types and functions. However, such restrictions often impose unnatural representations of data structures like lists or trees. The declarative characteristic of FRP and these restrictions impel us to write poorly maintainable redundant codes or deter us from writing certain types of programs. In this paper, we propose EmfrpBCT, an extended Emfrp with size-annotated recursive data types, to overcome this problem. The proposed system is more expressive than Emfrp, yet, it retains the aforementioned static properties. After explaining that through examples, we describe the features of EmfrpBCT, formalize the language, present an algorithm for statically computing the runtime memory bounds, and prove its soundness. Moreover, we implemented a compiler from EmfrpBCT to C, measured the translation time, and evaluated runtime overhead.

DOI： 10.2197/ipsjjip.29.685

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：ACM  

DOI： 10.1145/3457784.3457795

researchmap

その他リンク： https://dblp.uni-trier.de/db/conf/icsca/icsca2021.html#SakuraiMW21

記述言語：日本語   掲載種別：研究論文（学術雑誌）   出版者・発行元：日本ソフトウェア科学会  

DOI： 10.11309/jssst.38.2_20

Scopus

CiNii Books

CiNii Research

researchmap

その他リンク： https://ndlsearch.ndl.go.jp/books/R000000004-I031471020

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：SciTePress  

DOI： 10.5220/0007359305760583

researchmap

その他リンク： https://dblp.uni-trier.de/db/conf/icaart/icaart2019-2.html#TosueMT19

出版者・発行元：CEUR-WS.org  

researchmap

その他リンク： http://dblp.uni-trier.de/db/conf/comma/safa2018.html#conf/comma/KawasakiMT18

記述言語：英語   出版者・発行元：CEUR-WS.org  

researchmap

その他リンク： http://dblp.uni-trier.de/db/conf/comma/safa2018.html#conf/comma/MoriguchiT18

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

DOI： 10.5220/0006123404230430

Web of Science

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）  

DOI： 10.1587/transcom.2016NEP0013

Web of Science

researchmap

出版者・発行元：EasyChair  

researchmap

その他リンク： http://dblp.uni-trier.de/db/conf/sycss/scss2016.html#conf/sycss/MoriguchiGT16

記述言語：日本語   出版者・発行元：日本ソフトウェア科学会  

我々は対話的証明支援系Coqに対して，対話的修正機構という，既存の証明済みの体系に対する拡張をサポートする機構の提案を行った．提案した機構では，宣言した帰納型に対する新しい構成子の追加を可能としていた．しかし，この機構では既存の構成子や型，関数に対する新たなパラメータの追加は不可能であった．<BR>本論文では，レコードに対して新たなフィールドを追加する手法と，その場合のCoqにおける型システムの制限について分析する．この手法は，レコードだけでなく，構築子や関数に対するパラメータの追加も可能とするが，その場合の問題点についても述べる．

DOI： 10.11309/jssst.33.2_125

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

DOI： 10.1016/j.procs.2015.07.197

Web of Science

researchmap

記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

組込みシステム等において典型的に要求される性質に実時間制約がある.実時間制約は横断的関心事の1つであり,プログラムを複雑にする.本研究の目的は,文脈指向プログラミングの考え方に基づいた実時間制約の記述方式とそのモジュール化手法,およびそれに基づくプログラミング言語の提案である.実時間システムのプログラムは,外部環境などの変化に加え,時刻および時間経過に依存する振舞いを示すプログラムと考えることができる.そこで我々は時刻や時区間を文脈と見なすことで,文脈指向プログラミングの考え方を用いた実時間制約の記述方式を提案する.さらに時間の経過は位置情報などの外部要因による文脈の変化と同様にとらえることができるため,我々は時間の経過をイベントとしてとらえ,EventCJのような状態遷移モデルに基づく文脈の活性化制御を導入した.以上の考え方に基づいて設計された言語ProcneJでは,状態遷移を宣言するプロセス記述と実行可能なコードを記述するク

researchmap

出版者・発行元：ACM  

DOI： 10.1145/2480362.2480594

researchmap

その他リンク： http://dblp.uni-trier.de/db/conf/sac/sac2013.html#conf/sac/MoriguchiW13

記述言語：日本語   出版者・発行元：情報処理学会  

定理証明支援系Coqに対する，対話的にプログラムの変更・修正を行うための手法を提案し，その手法をCoqに組み込んだECoqを実装する．定理証明支援系によるプログラムの検証は，プログラムがある性質を満たすという証明により行われる．この証明はプログラムの構造や記述と非常に強く結び付いているため，プログラムを変更した場合，証明もまたその変更に依存した変更を行わなければならない．しかし，プログラムと証明の一貫性を保つために必要な変更箇所は，たとえばコンストラクタの追加という簡単な変更に限った場合であっても，既存の証明支援系では見つけにくい場合がある．このような問題に対処するため，我々はCoqで検証を行ったプログラムと証明に対して，その一貫性を保ちつつ変更するための手法を提案する．本論文で提案する手法では，コンストラクタの追加を行い，変更が必要な箇所を利用者に提示する．このとき，コンストラクタを追加する型だけではなく，宣言時の状態やその型を利用する他の型などの情報を用いるため，本手法はCoqの内部に組み込むことを前提としている．この機能は，変更が必要な箇所を対話的に修正するものであるため，我々はこれを対話的修正機構と呼ぶ．本論文で紹介するECoqは，コンストラクタの追加を行うコマンドをCoqに追加したものである．ECoqを用いることで，利用者はソースコードに直接コンストラクタを追加して得られるエラーメッセージより細かい粒度での情報が得られる．特にECoqは，通常決してエラーが起こらないが，修正する可能性のある箇所を指摘することで，利用者が修正箇所を見つける補助を行う．本論文では，例題を通じてエラーメッセージが出ない箇所をECoqが提示できることを確認する．It is generally difficult to extend or modify an already-verified program while maintaining the consistency of the program itself and its accompanying proofs of certain desirable properties. In this paper, we propose a novel method to support the process of modifying verified programs by interactively correcting the program definitions and proofs developed with Coq proof assistant. For this method, we introduce ECoq, our extended version of Coq equipped with a component called interactive correction mechanism. The mechanism described in this paper deals with the addition of new constructors to existing inductive types and then tries to locate prospective correction points within the modified program and its proofs. Thanks to this mechanism, our method enables us to find such correction candidates more accurately than usual process guided by error messages of Coq. In particular, ECoq can point out some correction candidates that do not originate any errors.

CiNii Books

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

Web of Science

researchmap

記述言語：日本語   出版者・発行元：日本ソフトウェア科学会  

CiNii Books

CiNii Research

researchmap

記述言語：日本語   出版者・発行元：日本ソフトウェア科学会  

researchmap

記述言語：日本語  

定性空間表現PLCAを帰納的に定義することでモデル化し，このモデルの集合が平面性を満たすPLCAの集合と一致していることを，証明支援系Coqを用いて証明する．PLCAは，空間データに対して，それを構成する点（Point），線（Line），周（Circuit），範囲（Area）というオブジェクトを用いそれらの包含関係によってそれを表現する手法である．この表現は座標データを用いずに領域同士の接続関係を定性的に表すもので，空間データ上に関して焦点をしぼった推論ができる．推論の正当性を保証するためには，PLCAと空間データの対応関係を証明する必要があるが，与えられたPLCA表現が二次元平面に埋め込めるための条件は示されているものの，平面性を満たすPLCAの集合を帰納的に構築する方法については議論されていない．本発表では，まず，3つの構成子を用いてPLCAを帰納的に定義し，これらによって構築されるモデルが平面性条件を満たすことを証明する．証明は，帰納法に基づき，各構成子に対して場合分けして行う．また，平面性条件を満たすPLCAと表現上等価な帰納的PLCAが構築できることを範囲の数に関する帰納法を使って証明する．証明では，範囲の数を増やしたときのPLCAの型を平面性条件から得られるものと一致させる必要があり，帰納の仮定となるPLCAを適切に設定することで証明の道筋を得ることができた．We give a model to a qualitative spatial representation PLCA by formalizing it inductively, and prove that such a model coincides with the planar PLCA, using a proof assistant Coq. PLCA provides a symbolic expression of spatial entities and allows reasoning on this expression. To justify the reasoning, we should prove the correspondence between PLCA expression and spatial data; for a given PLCA expression, the conditions for planarity have been shown, but the construction of such a PLCA expression has not been discussed. In this presentation, we give an inductive definition to PLCA with three constructors, and prove that the obtained model satisfies the conditions for planarity. The proof is based on induction and using case split on each constructor. On the other hand, we prove that an inductive PLCA can be constructed that is equivalent to a planar PLCA expression, using an induction on the number of areas. In the proof, we should match the type of PLCA with the succeeding number of the areas with that obtained by the conditions for planarity. Taking an appropriate PLCA as an induction hypothesis has solved this problem and guided us to get the proof.

CiNii Books

researchmap

記述言語：日本語  

Content-Centric Networking（CCN）とは2009年にVan Jacobsenが提案した通信方式であり，アドレスを利用するのではなくコンテンツ名に注目して通信を行うものである．CCNでは中継ノードでコンテンツをキャッシュすることができ，ネットワークの利用効率の向上や，応答時間の短縮が特徴としてあげられる．現在はシミュレーションをベースとして動作や性能のチェックが行われているが，CCNは確立した技術ではないため，実用化にむけて動作の正当性の検証が望まれる．本発表では，証明支援系Coqを用いて，CCNのプロトコルを帰納的にモデル化し，二分木のツリー型ネットワークトポロジにおいて動作の正当性の検証をした．このモデルでは，各ノードで行われているマッチング処理を実装し，1つの時系列リストを用意して，ノード間のパケットの送受信すべてを管理するようにした．動作の正当性として，あるコンテンツがネットワーク上に存在し，ユーザがそれを要求すれば，必ず正しいものを受信できるかということと，その逆の，コンテンツを受信した場合は，そのユーザが要求を送っていたということを証明した．Content-Centric Networking (CCN) is a communication architecture which was developed by Van Jacobsen on 2009. Communication on CCN is based on the names of objects, rather than on addresses. CCN can store contents on relay nodes. It is said that CCN improves network efficiency and reduces response time, but it is not a well-established technique. Although its behavior and performance are explored mainly by simulation, the behavioral correctness is required to be verified for its practical use. In this model, the matching process undertaken on each node is implemented and all events of sending/receiving packets are managed by a unique list. We proved two properties as behavioral correctness of this model on a binary tree topology. First, a user can retrieve the content if it sent the request under the condition that the content exists in the network. Second, a user must have been sent the request for the content if a user receives it under the condition that the content exists in the network. We have implemented the model and proved these properties using a proof assistant Coq.

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：[日本ソフトウェア科学会]  

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：神奈川大学総合理学研究所  

A case study of assurance case construction is presented. A formal assurance case for an embedded system life cycle is constructed. We also develop a framework for assurancecase construction. The structure of argument and ontology definition is prescribed by ourassurance case construction framework, which is based on the waterfall model of system development. The formal assurance case enables verification of consistency and integrity of the assurance case, and we indeed found some inconsistency arised as a result of a system update.原著

CiNii Books

CiNii Research

researchmap

記述言語：日本語  

組込みシステム等において典型的に要求される性質に実時間制約がある．実時間制約は横断的関心事の1つであり，プログラムを複雑にする．本研究の目的は，文脈指向プログラミングの考え方に基づいた実時間制約の記述方式とそのモジュール化手法，およびそれに基づくプログラミング言語の提案である．実時間システムのプログラムは，外部環境などの変化に加え，時刻および時間経過に依存する振舞いを示すプログラムと考えることができる．そこで我々は時刻や時区間を文脈と見なすことで，文脈指向プログラミングの考え方を用いた実時間制約の記述方式を提案する．さらに時間の経過は位置情報などの外部要因による文脈の変化と同様にとらえることができるため，我々は時間の経過をイベントとしてとらえ，EventCJのような状態遷移モデルに基づく文脈の活性化制御を導入した．以上の考え方に基づいて設計された言語ProcneJでは，状態遷移を宣言するプロセス記述と実行可能なコードを記述するクラス記述を分離することで，実時間制約に関する記述のモジュール化を可能にしている．さらにプロセス記述から時間オートマトンを生成することで，時間制約や層の活性化に関する性質のUPPAALによる検証を可能にしている．本発表では，提案手法の基本的アイデアについて説明し，例題を通して文脈指向の考え方による実時間制約記述の有効性について議論する．Real-time constraints are required typically in embedded systems. They can be regarded as crosscutting concerns and thus make real-time programs bulky. The goal of this work is to propose a description method of real-time constraints and their modularization technique using the idea of context-oriented programming. We also design a programming language ProcneJ for real-time systems based on the method. It is natural to think that a real-time (embedded) program depends not only on its changing runtime environment, but also on the passage of time. Thus we regard time points and time intervals as contexts and their changes as events to apply the idea of event-based context-oriented programming (as EventCJ) to real-time programs. In our language ProcneJ, separating the descriptions of event-based state transitions and class definitions enables modular development of real-time programs. In addition, by generating timed automata from the state transition parts, we can verify the consistency of real-time constraints using UPPAAL model checker. In the presentation, we will present the basic idea of our method and will show how it is beneficial for describing real-time systems through examples.

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：[日本ソフトウェア科学会]  

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：[日本ソフトウェア科学会]  

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

証明支援系 Coq のプログラムに対する対話的修正機構を提案する.証明支援系はプログラムなどの正しさを証明するために利用されている.しかし,Coq による証明は対象となる体系の定義に密接に関連しているため,定義のわずかな修正に対して多くの不整合が発生する.このような不整合に対し,場所の確認を Coq からのエラーによって発見するという,退屈で,かつ誤りを組み込みやすい作業で行うことが一般的になっている.提案する機構を組み込んだ証明支援系を用いることにより,この作業を簡易化することができる.対話的修正機構は修正箇所の記述を受け取ることで,その修正によって不整合が生じた箇所を提示することができる.また,この提示された箇所をもとに修正を対話的に行うことを可能にしている.本発表で提案している Coq における対話的修正機構では,帰納型に新たなコンストラクタを追加することと,そのコンストラクタに対応するデストラクタの拡張を行う機能を持っている.こ

researchmap

記述言語：日本語   出版者・発行元：情報処理学会  

我々はMorrisのアルゴリズムのCによる実装の検証を試みた．このアルゴリズムは再帰やスタックを用いずに二分木の走査を行うものであり，節点内部に余分なタグも不要であるという特徴がある．本研究はポインタ操作を伴うCプログラムへの検証支援ツール適用のケーススタディであり，今回は検証支援系CaduceusおよびWhy，自動証明系Simplifyおよび対話的証明支援系Coqを使用した．本稿では，これらによる検証手法とその結果の概要を述べる．We proved the partial correctness of a C implementation of Morris's tree traversal algorithm. The algorithm is known as a recursion-free, stack-free and tag-free binary tree traversal. This work is intended to be a case study of verifying C programs with pointer manipulation using existing verification tools such as Caduceus, Why, Simplify and Coq. In this report, we describe the outline of the verification methodology and results.

CiNii Books

researchmap

記述言語：日本語  

我々は，Morrisの2分木走査アルゴリズムのCによる実装を対象として，証明支援系を用いた正当性の検証を試みた．本論文はその手法と結果に関する報告である．Morrisのアルゴリズムは，ポインタの書き換えを行うことで再帰やスタックを用いずに2分木走査を行う方法のひとつである．また他のポインタ反転法と異なり節点に印を付けるためのビットを設ける必要もないのが特徴である．我々は，入力および走査結果についての仕様を事前・事後条件として与え，C用の検証支援ツールであるCaduceusによって検証条件を生成した．ループ不変条件は必要に応じて適宜与えた．生成された検証条件を自動検証ツールSimplifyおよび証明支援系Coqを用いて証明した．

researchmap

記述言語：日本語   出版者・発行元：一般社団法人電子情報通信学会  

ポインタ書き換えを伴うプログラムのプログラム変換にもとづく検証のケーススタディとして,Morrisの二分木走査アルゴリズムの正当性を扱った.本稿ではその際に用いたプログラム変換手法とその具体的な適用手法について報告する.

CiNii Books

researchmap

記述言語：日本語  

アスペクト指向が提案されて十余年たち，ソフトウェア工学の広い分野で用いられている．しかしながら，アスペクトとは何であるかを議論することはほとんどなく，ただAspectJに代表されるジョインポイントモデルにおけるモジュールをアスペクトとすることが多い．このように本質を定義しないままの議論は実際の言語に強く依存したものとなり，またツールにおけるアルゴリズムとその実装もアドホックになる．アスペクト指向はモジュール化を主眼としたものであり，その特徴はアスペクトモジュールの結合方法にあるといえる．本研究では，この結合方法を抽象化および定式化し，アスペクト指向の理解や議論の基礎とすることを目標としている．本研究の特徴はアスペクト指向言語のとらえ方にある．現存するアスペクト指向言語は，既存の言語に対して拡張を施すことによって作成されている．一方，既存研究ではアスペクト指向言語を1) ラムダ計算のような既存の計算体系にアスペクト指向を加えたもの，または2) 言語全体を記述する体系で定式化している．それに対し，本研究では2) と同様に既存の計算体系に依存せずにアスペクト指向としての操作の定式化のみを行い，他の体系との組合せによって1のように言語を表現する．本発表では，アスペクト指向における操作の定式化と，ラムダ計算との組合せによる言語の定式化，および他研究における議論の表現について述べる．Aspect-orientation has gained in software development in the last decade. However, formal and/or general definitions of aspects and related concepts are not thoroughly discussed so far. The important concepts such as aspect, join point, pointcut, advice, etc. are defined on top of specific aspect-oriented languages such as AspectJ. Our goal is to formalize some'aspectual'operations commonly used in aspect-oriented languages. We designed a simple calculus that models the operations independently from other computational activities such as function application or message passing. We can easily construct a model of a specific aspect-oriented language by mixing our calculus with another model that represents the base computation. In this presentation, we give a formalization of the aspectual operations in our calculus and then discuss the formalization by comparing to other works.

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

アスペクト指向が提案されて十余年たち,ソフトウェア工学の広い分野で用いられている.しかしながら,アスペクトとは何であるかを議論することはほとんどなく,ただAspectJに代表されるジョインポイントモデルにおけるモジュールをアスペクトとすることが多い.このように本質を定義しないままの議論は実際の言語に強く依存したものとなり,またツールにおけるアルゴリズムとその実装もアドホックになる.アスペクト指向はモジュール化を主眼としたものであり,その特徴はアスペクトモジュールの結合方法にあるといえる.本研究では,この結合方法を抽象化および定式化し,アスペクト指向の理解や議論の基礎とすることを目標としている.本研究の特徴はアスペクト指向言語のとらえ方にある.現存するアスペクト指向言語は,既存の言語に対して拡張を施すことによって作成されている.一方,既存研究ではアスペクト指向言語を1) ラムダ計算のような既存の計算体系にアスペクト指向を加え

researchmap

記述言語：日本語   出版者・発行元：一般社団法人電子情報通信学会  

アスペクト指向プログラミング(AOP)はソフトウェア開発において広く用いられており、アスペクト指向プログラミング言語のもつ性質を形式的にとらえ、理解することはプログラミング言語研究の重要な課題のひとつである。我々は、ポイントカットやアドバイスといったアスペクト指向言語拡張の性質をとらえることを目的とした計算体系LMCを提案する。LMCは特定のプログラミング言語に依存しない形で定義されており、これをアスペクト指向言語拡張の定義に用いることで、アスペクト指向プログラミング言語の形式的定義をモジュール化できる。本論文ではLMCの定義の概要を示し、アスペクト指向拡張をもつ簡単なオブジェクト指向言語をLMCを用いて形式的に定義する。

CiNii Books

researchmap