Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：ACM  

DOI： 10.1145/3651781.3651789

researchmap

Other Link： https://dblp.uni-trier.de/rec/conf/icsca/2024

Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：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

Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：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

Language：English   Publishing type：Research paper (international conference proceedings)  

DOI： 10.1145/3594671.3594674

researchmap

Other Link： https://dblp.uni-trier.de/db/conf/programming/programming2023.html#SuzukiWM23

Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：ACM  

DOI： 10.1145/3563837.3568338

researchmap

Language：English   Publishing type：Research paper (scientific journal)   Publisher：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

Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：ACM  

DOI： 10.1145/3457784.3457795

researchmap

Other Link： https://dblp.uni-trier.de/db/conf/icsca/icsca2021.html#SakuraiMW21

Language：Japanese   Publishing type：Research paper (scientific journal)   Publisher：Japan Society for Software Science and Technology  

DOI： 10.11309/jssst.38.2_20

Scopus

CiNii Books

CiNii Research

researchmap

Other Link： https://ndlsearch.ndl.go.jp/books/R000000004-I031471020

Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：SciTePress  

DOI： 10.5220/0007359305760583

researchmap

Other Link： https://dblp.uni-trier.de/db/conf/icaart/icaart2019-2.html#TosueMT19

Publisher：CEUR-WS.org  

researchmap

Other Link： http://dblp.uni-trier.de/db/conf/comma/safa2018.html#conf/comma/KawasakiMT18

Language：English   Publisher：CEUR-WS.org  

researchmap

Other Link： http://dblp.uni-trier.de/db/conf/comma/safa2018.html#conf/comma/MoriguchiT18

Language：English   Publishing type：Research paper (international conference proceedings)  

DOI： 10.5220/0006123404230430

Web of Science

researchmap

Language：English   Publishing type：Research paper (scientific journal)  

DOI： 10.1587/transcom.2016NEP0013

Web of Science

researchmap

Publisher：EasyChair  

researchmap

Other Link： http://dblp.uni-trier.de/db/conf/sycss/scss2016.html#conf/sycss/MoriguchiGT16

Language：Japanese   Publisher：日本ソフトウェア科学会  

We introduced an interactive extension mechanism, which allows us to extend programs and systems verified with Coq. In the mechanism, only adding new constructors into existing inductive types are allowed, but adding parameters into functions or constructors are not.<BR>In this paper, we introduce a novel mechanism, which allows us to add new fields into record types. We also show the limitations of the mechanism arising from the type system of Coq. The method used in the mechanism is also applicable for adding parameters to existing constructors and functions. We explain problems occurring when we apply the method into them.

DOI： 10.11309/jssst.33.2_125

researchmap

Language：English   Publishing type：Research paper (international conference proceedings)  

DOI： 10.1016/j.procs.2015.07.197

Web of Science

researchmap

Language：Japanese   Publisher：一般社団法人情報処理学会  

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 examp

researchmap

Publisher：ACM  

DOI： 10.1145/2480362.2480594

researchmap

Other Link： http://dblp.uni-trier.de/db/conf/sac/sac2013.html#conf/sac/MoriguchiW13

Language：Japanese   Publisher：情報処理学会  

定理証明支援系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

Language：English   Publishing type：Research paper (international conference proceedings)  

Web of Science

researchmap

Language：Japanese   Publisher：日本ソフトウェア科学会  

CiNii Books

CiNii Research

researchmap

Language：Japanese   Publisher：日本ソフトウェア科学会  

researchmap

Language：Japanese  

定性空間表現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

Language：Japanese  

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

Language：Japanese   Publisher：[日本ソフトウェア科学会]  

CiNii Books

researchmap

Language：Japanese   Publisher：神奈川大学総合理学研究所  

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

Language：Japanese  

組込みシステム等において典型的に要求される性質に実時間制約がある．実時間制約は横断的関心事の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

Language：Japanese   Publisher：[日本ソフトウェア科学会]  

CiNii Books

researchmap

Language：Japanese   Publisher：[日本ソフトウェア科学会]  

CiNii Books

researchmap

Language：Japanese   Publisher：一般社団法人情報処理学会  

We propose an interactive refinement mechanism for Coq proof assistant, which aims to improve the reusability of proof scripts. Suppose that we have some proof scripts about a computer program. We call the program the proof target of the proof scripts. The problem is that it is generally difficult to reuse the scripts for a modified proof target. Even some small changes, such as just adding new constructors to some inductive types, could cause a large number of inconsistencies in the scripts. Usually we should manually find and fix them by examining error messages issued by the proof assistant, which is hard and error-prone process. Using the proof assistant modified to incorporate the proposed mechanism can ease the process. By providing the modified part of the target definition, our interactive refinement mechanism finds all the inconsistent parts in the definition and the proof scripts. After finding them, we can easily gain the proofs for the new target by issuing correction commands to the modified proof assistant. The interactive refinement mechanism for Coq described in this presentation covers the extension of inductive data types with new constructors and the destructors

researchmap

Language：Japanese   Publisher：情報処理学会  

我々は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

Language：Japanese  

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

researchmap

Language：Japanese   Publisher：The Institute of Electronics, Information and Communication Engineers  

We proved the 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 by using program transformation. In this report, we describe the outline of the verification methodology and results.

CiNii Books

researchmap

Language：Japanese  

CiNii Books

researchmap

Language：Japanese   Publisher：一般社団法人情報処理学会  

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.

researchmap

Language：Japanese   Publisher：The Institute of Electronics, Information and Communication Engineers  

Aspect-oriented programming (AOP) has gained wide popularity in software development. Understanding the formal nature of aspect-oriented languages is one of the pressing problems in programming language research. We are currently developing LMC, a calculus intended to capture the properties of commonly used aspectual language extensions such as pointcut and advice. We define LMC to be independent from particular languages. LMC can emphasize the modularity in the formal definitions of aspect-oriented languages by using the calculus to define the aspectual parts of their semantics. In this paper, we introduce LMC and show how to use it to define a simple object-oriented language with aspect-oriented extensions.

CiNii Books

researchmap