Authorship：Last author,　Corresponding author   Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：Atlantis Press  

Computational systems that deal with discrete time, such as stream computations and synchronous data flow languages, can be modeled using lists. However, most list operations are on finite lists, and it is not easy to define them for infinite lists to express persistent behavior. In particular, when using theorem provers, intuitive definitions are unacceptable due to restrictions on the handling of infinities. When integrating computational failures into the system, existing research either directly expresses failures or utilizes a mechanism that continues to send invalid values indefinitely. Still, the latter cannot determine failures in terms of computation. In this study, we formalize a model of a reversible synchronous dataflow language using finite and infinite lists and show that the semantics of each correspond to each other using the Coq theorem prover. For infinite lists, the inconsistency that arises as a result of incorporating failures into the list is resolved using finite lookahead.

DOI： 10.2991/978-94-6463-684-0_2

researchmap

Authorship：Last author,　Corresponding author   Language：Japanese   Publishing type：Research paper (scientific journal)   Publisher：JSSST  

XStorm, an FRP language for small-scale embedded systems, allows us to concisely describe state-dependent behaviors based on the state transition model. However, when we use different sets of peripheral devices depending on states, device management, such as switching power modes, should be implemented in a driver code in C. This would result in bugs as inconsistency between the state in the XStorm program and that in the driver code cannot be detected. In this research, we extend XStorm’s state hook model to express modes of peripherals that depend on states. By the extension, the language manages modes of peripherals, and thus the inconsistency is statically avoided.

DOI： 10.11309/jssst.42.1_40

researchmap

Authorship：Last author   Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：Information Processing Society of Japan  

Emfrp is a functional reactive programming (FRP) language for resource-constrained systems such as microcontrollers. The language enables the concise description of reactive behavior specific to embedded systems. The current Emfrp compiler runs on a development host PC. Therefore, the program development, testing, and modification cycle is time-consuming. We have implemented an interpreter, Emfrp-REPL, which runs on the target device and enables interactive and rapid development using the REPL interface. The interpreter is designed to minimize I/O latency and employs snapshot GC to suppress latency fluctuations. However, the execution speed could be faster because the evaluation of expressions is based on AST traversal. In this study, we design and implement Emfrp-VM, a byte code VM for Emfrp, to solve this problem.

researchmap

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

As IoT devices advance, their microcontroller systems-on-a-chip (SoCs) demand higher speeds, more memory, and advanced peripherals, leading to increased power consumption. Integrating low-power (LP) coprocessors in SoCs can reduce power usage while maintaining responsiveness. However, switching application execution to and from the coprocessors generally involves complex and platform-specific procedures. We propose a JIT compilation method for managed programming languages to streamline LP coprocessor use. Our prototype for the programming language mruby includes a JIT compiler and a seamless processor-switching mechanism, enabling rapid development of IoT applications leveraging LP coprocessors. This work-in-progress paper describes the design and implementation of the extended mruby interpreter and presents preliminary evaluations of its power consumption and latency on ESP32-S3 and ESP32-C6.

DOI： 10.1145/3679007.3685064

researchmap

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

関数リアクティブプログラミング（FRP）は，時間と共に変化する値である時変値を宣言的に組み合わせることによってリアクティブシステムを記述するプログラミングパラダイムである． 組込みシステム向けFRP言語であるEvEmfrpは，時変値に対しその更新タイミングを型情報として持たせることで周期的・非周期的なタスク処理を記述することができる． しかし，それぞれの時変値の更新がいつ完了するかといった実時間性に関する保証がなく，リアルタイムシステム向けの言語としては十分ではない． 本研究では，EvEmfrpをもとに，リアルタイムシステムを記述するための構文を備えたFRP言語を提案する． 本言語では，明示的にタスクとそのデッドラインを記述することができ，各タスクでどの時変値が更新されるかを時変値が持つタイミングから静的に決定することができる． また，本言語におけるタスク処理に適したスケジューリング機構を提案する．

researchmap

Authorship：Last author   Language：Japanese   Publishing type：Research paper (scientific journal)   Publisher：JSSST  

DOI： 10.11309/jssst.41.3_34

researchmap

Authorship：Last author   Language：Japanese   Publisher：情報処理学会  

Emfrpはマイクロコントローラなどの小規模組込みシステム向けに設計された関数リアクティブプログラミング(FRP)言語であり，組込みシステム特有のリアクティブな動作の簡潔な記述を可能にする． その処理系は開発用のホストマシン上で動作するクロスコンパイラであり，プログラムの修正・テストのサイクルに時間がかかる． そこで我々はターゲットデバイス上で動作し，REPLによる対話的かつ迅速な開発を可能にするインタプリタEmfrp-REPLを実装した． Emfrp-REPLではI/Oレイテンシを低く抑える工夫がなされており，スナップショットGCによってレイテンシの変動を抑制しているが，式の評価がASTの走査によるため実行速度にやや難がある． 本研究ではEmfrpのためのバイトコードVMにもとづく処理系Emfrp-VMを設計・実装し，この問題の解決を図る．

researchmap

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

Emfrp, a functional reactive programming (FRP) language for small-scale embedded systems, is a DSL designed for execution in resource-constrained environments.
The execution model of Emfrp provides a reactive behavior of the system through repeated actions such as waiting for inputs from sensors, updating all time-varying values, and outputting them to the actuators.
Such polling-based execution consumes unnecessary energy due to frequent update processing.
For this reason, the extended language EvEmfrp was proposed to reduce unnecessary update processing and improve energy consumption.
EvEmfrp statically determines and schedules the update period of the whole system by annotating the timing of the time-varying value updates and the input interrupts.
Since time-varying value updates are performed at periodic timing, the system is put into sleep mode when no update processing is required, thereby saving energy.
However, because the timing annotations and the update intervals are set statically, executing a program that updates a specified time-varying value after a fixed time starting from an interrupt signal without unnecessary updates is impossible.
This causes frequent wake-up from sleep mode and prevents power saving.
We propose a mechanism for extending timing annotations and dynamically changing the update intervals to solve this problem.
We also show the usefulness of the proposed mechanism through an example of debouncing for button presses.

DOI： 10.1145/3651781.3651789

researchmap

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

DOI： 10.2991/978-94-6463-388-7_10

researchmap

Authorship：Last author   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

Authorship：Last author   Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：IPSJ  

A low power coprocessor in the microcontroller helps to save total power consumption. While the main processor is in a sleep state, the low power coprocessor can process the inputs and maintain responsiveness. However, inter-processor communication and processor power state management make development more complicated. In this paper, we address this problem by introducing a mechanism to switch a running processor to the functional reactive programming (FRP) language XStorm, which has an abstraction mechanism for modeling stateful behaviors. The proposed mechanism allows us to choose which processor to run in each state. Therefore, the switching of a running processor can be represented as a state transition. Our compiler can absorb differences in processor architectures and automatically generate programs for inter-processor communication and processor state management. As a result, developers can more easily describe system with coprocessors. We describe the proposed mechanism and report an evaluation on the power consumption and time of state transitions.

researchmap

Authorship：Last author,　Corresponding author   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

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

This paper reports the implementation of Emfrp-REPL, an interactive interpreter (REPL) of a functional reactive programming language for resource-constrained embedded systems. Its goal is to accelerate the prototyping and development of microcontroller-based embedded systems. The interpreter runs on small-scale embedded devices based on 32-bit microcontrollers, such as ESP32 with 520KiB size data RAM. The evaluation shows that the memory usage of Emfrp-REPL is comparable to MicroPython, and the range of its latency is narrower than MicroPython, according to microbenchmarks.

DOI： 10.1145/3594671.3594674

researchmap

Authorship：Last author,　Corresponding author   Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：ACM  

Emfrp is a functional reactive programming language designed for small embedded systems. By imposing certain restrictions on the language mechanism, the language guarantees the termination of the update process for each time-varying value and enables static determination of the amount of memory required for execution. This allows Emfrp programs to run safely even in resource-constrained execution environments. However, the abovementioned restrictions make it difficult to write time-consuming operations (heavy tasks) such as graph structure construction and exploration based on external data. Moreover, since Emfrp updates time-varying values synchronously, a naive implementation of such heavy tasks using external function calls will result in a slow response time to input. Some existing programming languages provide asynchronous processing mechanisms to ensure descriptiveness and responsiveness for heavy tasks. In this study, we propose a method to introduce heavy tasks into reactive programs naturally by introducing language mechanisms equivalent to asynchronous processing mechanisms, such as future and promise, into Emfrp. In this paper, we first discuss the problems with a naive implementation of heavy tasks in Emfrp, then explain the proposed method based on an example, and discuss the language runtime implementation.

DOI： 10.1145/3563837.3568338

researchmap

Authorship：Last author,　Corresponding author   Language：English  

researchmap

Authorship：Last author,　Corresponding author   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

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

Wireless Sensor and Actor Networks (WSANs) are distributed systems composed of multiple computers that observe and act on physical environments. Since WSANs contain actor nodes that control actuators or perform other local operations, complex inter-node coordination operations involving them are necessary. The lack of such coordination may result in the incorrect arrival order of messages between actor and sensor nodes. The problems are called hazards. For wireless sensor networks (WSNs), which do not have actor nodes, there is a method called macro-programming, which describes the behavior of the entire WSN as a single computing system. In macro-programming, inter-node cooperation for processing is derived from the overall behavior. In this study, we propose a macro-programming language for WSAN that incorporates a mechanism to derive cooperative actions to avoid hazards.

researchmap

Authorship：Lead author,　Corresponding author   Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：IPSJ  

Functional reactive programming (FRP) is a programming paradigm where a system is described using declarative abstractions of the change propagation of discrete events and continuous signals. This paper presents a purely functional reactive programming model that facilitates a uniform description of distributed coordination and per-node computation. A case study of a wireless sensor-actor network (WSAN) shows that both inter-node coordination and intra-node computation can uniformly be written as reactive behaviors. The paper also describes an implementation method of the model using Distributed XFRP, a pure FRP language for distributed systems.

researchmap

Authorship：Last author,　Corresponding author   Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：ACM  

We propose new functionality for FRP language to support computations on GPUs. Some embedded systems equip GPUs, which enable us to process large amounts of data such as camera images. We have developed an FRP language for embedded systems, named Emfrp. However, Emfrp lacks two kinds of concepts for computations on GPUs; one is the representation for large amounts of data, and the other is the declaration of the calculational resources of computations. In this paper, we introduce node arrays and GPU nodes, which are time-varying values computed on GPUs. We also show a prototype language of these features and evaluation through some examples on it.

DOI： 10.1145/3457784.3457795

researchmap

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

researchmap

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

researchmap

Authorship：Last author,　Corresponding author   Language：Japanese   Publishing type：Research paper (conference, symposium, etc.)   Publisher：情報処理学会  

関数リアクティブプログラミング (FRP) は，時間とともに変化する値（時変値）間の依存関係を副作用のない式で表すことで，リアクティブな動作の宣言的な記述を支援するプログラミングパラダイムである．本研究では，組込みシステム向けに設計されたFRP言語LRFRPを提案する．LRFRPはプログラミング言語Rust上の内部DSLであり，Rustのマクロ機能を用いて実装されている．Rustプログラム中に埋め込まれたLRFRPのプログラムは，コンパイル時にRustのモジュールに変換される．このモジュールは極めて限られたライブラリにのみ依存し，またRustの機能を制限しない．そのため，組込みシステムをターゲットとする場合など，利用できるライブラリが限定された状況でも動作可能である．本稿ではLRFRPの概要と実装方式について述べ，例を通してその有効性について議論する．

CiNii Research

researchmap

Authorship：Last author,　Corresponding author   Language：Japanese   Publishing type：Research paper (scientific journal)   Publisher：Information Processing Sociey of Japan  

Embedded systems are classified as reactive systems, which respond to external input and update their states. Developing such systems tend to be complicated because many of those systems change their behavior depending on the internal states. To support developing embedded reactive systems, we propose an abstraction mechanism that provides a method to express state-dependent behaviors in the style of Functional Reactive Programming (FRP). Specifically, we introduce a variant of switch-extension to Emfrp, an FRP language designed for small-scale embedded system. This extension provides a mechanism to define time-varying values and state transitions for each state. It enables us to describe stateful reactive systems in a declarative way. Also, the language targets small-scale embedded systems such as microcontrollers. Thus, dynamic memory allocation is not desirable because it may cause runtime error due to unpredictable memory consumption. The proposed extension statically defines the set of states included in transitions to limit possible behaviors. We implement the switch-extension as the source-code translation to pure Emfrp codes. We show an example to demonstrate that the extension adequately modularizes stateful components.

researchmap

Other Link： https://www.psg.c.titech.ac.jp/posts/2020-04-27-IPSJPRO.html

Authorship：Last author,　Corresponding author   Language：Japanese   Publishing type：Research paper (conference, symposium, etc.)  

関数リアクティブプログラミング(FRP)言語Emfrpに対する再帰的なデータ型の導入手法を提案する． Emfrpはマイクロコントローラのような小規模システム向けに設計された純粋FRP言語である． この言語では，関数やデータ型の再帰的な定義を禁止する等の言語的制約を課すことで， 時変値の更新処理が停止することや実行時に必要なメモリサイズを静的に決定できることが保証される． 本研究では型に対してサイズの情報を含めることで，Emfrpの性質を維持しつつこの制約を緩和する手法を提案する．

researchmap

Authorship：Last author,　Corresponding author   Language：English   Publishing type：Part of collection (book)   Publisher：Springer International Publishing  

This paper presents a functional reactive embedded domain-specific language (EDSL) for resource-constrained embedded systems and its efficient execution method. In the language, time-varying values changes at discrete points of time rather than continuously. Combined with a mechanism to let users designate the update interval of values, it is possible to derive the minimal value-updates required to produce the user-desired output. Also, the event-driven backend asynchronously updates an input value when its value is required. In this way, we can greatly reduce the number of updates.

DOI： 10.1007/978-3-030-26428-4_12

researchmap

Authorship：Corresponding author   Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：ACM Press  

This paper presents an automatic parallelization method for a pure FRP language designed for embedded systems. Recent advances in microprocessor technology make it possible to use multicore processors even in resource-constrained embedded systems. To fully utilize such processors with a pure FRP language, we propose a method for parallelizing signal graph updates. The method is based on a static scheduling algorithm because it should run with a simple RTOS or without the help of operating systems. To evaluate the proposed method, we implemented a parallelizing compiler for XFRP, a pure FRP language for embedded systems. In this paper, we describe the parallelizing method and show some preliminary evaluation results using Linux-based systems that demonstrate the effectiveness of the method.

DOI： 10.1145/3358503.3361276

researchmap

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

This paper introduces a reflective extension of a functional reactive programming language designed for resource-constrained embedded systems. Using the extension, a program module can observe or modify its execution process via time-varying values that are connected to the internal of the metalevel of the module. Thus reflective operations are also reactive and described in a declarative manner. An example shows how the mechanism can realize an adaptive runtime that reduces the power consumption of small robots.

researchmap

Language：Japanese   Publishing type：Research paper (conference, symposium, etc.)  

This paper briefly describes the design of a simple context-oriented programming extension to Emfrp, a purely functional reactive programming language for resource-constrained embedded systems. The proposed extension provides a layer mechanism along with a feature to describe events along with the layer activation. An example shows that the extension can eliminate typical cross-cutting code that often appear in plain Emfrp programs.

researchmap

Authorship：Lead author,　Corresponding author   Language：English   Publishing type：Research paper (international conference proceedings)  

This paper presents the design of a simple context-oriented programming extension to Emfrp, a purely functional reactive programming language for resource-constrained embedded systems. The language provides declarative and straightforward ways to describe various reactive behaviors in embedded systems. However, because of the static nature of the language, Emfrp lacks suitable capabilities to modularize adaptive behaviors. The proposed extension introduces a simple layer mechanism with implicit layer activation. It also provides a feature to describe responses to events that correspond to the moments of layer activations and deactivations. The extension can improve the modularity of Emfrp programs by separating the descriptions of context-dependent behaviors, and hence eliminating various cross-cutting code fragments.

DOI： 10.1145/3242921.3242925

researchmap

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

In this paper, we propose an implementation method of hygienic macro-definition mechanisms into languages defined using OMeta, an OOP language with PEG-based general-purpose pattern matching. From the specification of a macro-definition mechanism and a parser written in OMeta, the proposed method generates an extended parser equipped with the macro-definition mechanism based on the Scoped Set model. We show the effectiveness of the method by applying it to two different languages: Javascript and MinCaml.

DOI： 10.11309/jssst.35.2_33

researchmap

Language：Japanese   Publishing type：Research paper (conference, symposium, etc.)  

This paper briefly describes a new execution mechanism for an FRP language designed for resource constrained embedded systems. The mechanism is based on the Actor model, a concurrent computation model in which computation is achieved by actors communicating via asynchronous messages. We adopt actors for the run-time representation of time-varying values and event streams. With this representation, we can naturally integrate adaptable execution mechanism in the runtime of the language.

researchmap

Language：Japanese  

J-GLOBAL

researchmap

Language：Japanese  

J-GLOBAL

researchmap

Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：Institute of Electrical and Electronics Engineers Inc.  

DOI： 10.1109/SNPD.2017.8022750

Scopus

researchmap

Language：Japanese  

J-GLOBAL

researchmap

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

DOI： 10.1145/3079368.3079387

Scopus

researchmap

Publisher：ACM  

researchmap

Other Link： http://dblp.uni-trier.de/db/conf/agere/agere2017.html#conf/agere/ShibanaiW17

Language：Japanese  

J-GLOBAL

researchmap

Language：Japanese  

J-GLOBAL

researchmap

Language：Japanese  

J-GLOBAL

researchmap

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

DOI： 10.1145/2892664.2892670

Web of Science

researchmap

Other Link： http://dblp.uni-trier.de/db/conf/aosd/modularity2016c.html#conf/aosd/SawadaW16

Language：Japanese   Publisher：Japan Society for Software Science and Technology  

We present the notion of concurrent context-oriented programming and its implementation method. To realize context-oriented programming in concurrent systems based on asynchronous communication such as the Actor model, one must take special care to control synchronizations among context changes and other computations. Our method uses reflection to solve the synchronization problem regarding messages that cross two contexts. In this paper, we give some preliminary evaluation results using an implementation in Erlang.

DOI： 10.11309/jssst.33.1_167

J-GLOBAL

researchmap

Language：Japanese  

J-GLOBAL

researchmap

Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：Association for Computing Machinery, Inc  

DOI： 10.1145/2834965.2834972

Scopus

researchmap

Other Link： http://dblp.uni-trier.de/db/conf/middleware/arm2015.html#conf/middleware/TakenoW15

Language：Japanese  

J-GLOBAL

researchmap

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

Web of Science

researchmap

Language：English   Publishing type：Research paper (scientific journal)   Publisher：University of Cincinnati  

Scopus

researchmap

Language：Japanese  

CiNii Books

researchmap

Language：Japanese  

CiNii Books

researchmap

Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：Association for Computing Machinery  

DOI： 10.1145/2637066.2637069

Scopus

researchmap

Other Link： http://dblp.uni-trier.de/db/conf/ecoop/cop2014.html#conf/ecoop/WatanabeT14

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

DOI： 10.1007/978-3-319-08222-6

Scopus

researchmap

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

DOI： 10.1007/978-3-662-44471-9_3

Web of Science

researchmap

Language：Japanese  

CiNii Books

researchmap

Language：Japanese   Publisher：電子情報通信学会  

We adapt a formal approach for an investigation into robustness analysis on human-made faults in procedural manuals. Detection or recovery tasks for human-made faults are probably embedded into procedural manuals. The investigation of usefulness of the tasks is important to preserve the trust of workflows in safety critical domains. We define fault semantics of several human-made faults, and then inject the faults into the model of procedural manuals. After that, using model checking technique, we verify that the injected model satisfies a property as a goal.

CiNii Books

researchmap

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

本研究の目的は適応的実時間システムのためのドメイン固有言語 (DSL) の提案である.組込みシステム等に要求される性質である適応性と実時間性はいずれも横断的関心事であり,プログラムを複雑化する要因となる.適応的な振舞は実行時の環境を表す情報 (文脈) に依存する動作として記述できる.そしてそのような記述のモジュール化を促進する手法として文脈指向プログラミング (COP) が提案されている.我々は,時刻および時区間を文脈とみなすことで,COP の考え方が適応的実時間システムに有効であることを示している.従来,COP を支援する機構は言語処理系を拡張して導入されることが一般的であったが,本研究ではプログラミング言語 Scala の諸機能を用いて COP のための内部 DSL を実現することで,言語処理系を拡張することなく適応的実時間システムのモジュラーな記述が可能になることを示す.

CiNii Books

researchmap

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

DOI： 10.1145/2480362.2480594

Scopus

researchmap

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

Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：Association for Computing Machinery  

DOI： 10.1145/2541329.2541341

Scopus

researchmap

Other Link： http://dblp.uni-trier.de/db/conf/agere/agere2013.html#conf/agere/Watanabe13

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.

researchmap

Language：Japanese  

CiNii Books

researchmap

Other Link： http://id.nii.ac.jp/1001/00083703/

Language：Japanese  

CiNii Books

researchmap

Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：IEEE Computer Society  

DOI： 10.1109/SNPD.2012.115

Scopus

J-GLOBAL

researchmap

Other Link： http://dblp.uni-trier.de/db/conf/snpd/snpd2012.html#conf/snpd/SenthooranW12

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

Web of Science

researchmap

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

DOI： 10.1016/j.entcs.2006.07.002

Scopus

J-GLOBAL

researchmap

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

DOI： 10.1109/ARES.2006.114

Web of Science

J-GLOBAL

researchmap

Other Link： http://dblp.uni-trier.de/db/conf/IEEEares/ares2006.html#conf/IEEEares/NagatouW06

Language：Japanese   Publishing type：Research paper (scientific journal)   Publisher：社団法人情報処理学会  

In this paper, we report the design and implementation of Moxa-a behavioral interface specification language that supports DbC (Design by Contract) based specifications. In DbC methodology, a contract arranges responsibilities between a user and a supplier of the service. This improves software quality because this makes clear who has responsibility, how to use, and what is the result of the service. With JML (Java Modeling Language), a DbC based behavioral interface specification language for Java, we can declare assertions as pre/post-conditions for each method. However, as the number of methods increases and the functionalities of services become complex, assertions for each method gets complicated. This makes it difficult to keep the consistency between assertions and methods while we are modifying them. Using Moxa, we can divide and describe assertions into several modules called assertion-aspects, when we can regard the behavior of the object(s) as the composition of some independent aspects. In JML style specification declaration, the aspects are crosscut over the assertions declared for difference methods. In this paper, we show the modularization mechanism for assertion de

researchmap

Publisher：Fakultat fur Informatik, Universitat Magdeburg  

researchmap

Publisher：IASTED/ACTA Press  

researchmap

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

Web of Science

researchmap

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

DOI： 10.1109/WSTFES.2003.1201363

Web of Science

researchmap

Other Link： http://dblp.uni-trier.de/db/conf/wstfeus/wstfeus2003.html#conf/wstfeus/WatanabeYN03

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

DOI： 10.1007/3-540-36532-X_13

Web of Science

researchmap

Language：English   Publishing type：Research paper (scientific journal)   Publisher：日本ソフトウェア科学会  

DOI： 10.11309/jssst.20.292

Scopus

researchmap

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

Scopus

researchmap

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

Recently, mobile code technology has been utilized in many systems: Java applets, Jini, Active network, Internet appliances, etc. To make mobile code programs work more effectively, we must consider their adaptation on runtime environments. Our goal is to realize mobile code programs that can adapt themselves to runtime environments flexibly & safely. The adaptation can be regarded as a basic & important mechanism for software evolution of mobile code programs. Towards the goal, we design a software model named SAMcode. Mobile code programs based on the model can realize their adaptation on runtime environments successfully without their misbehavior & runtime errors and system faults. In this paper, we give an overview of the model and discuss its effectiveness.

DOI： 10.1145/512035.512050

researchmap

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

In a software system, dynamic adaptability is the ability for dynamic adaptation on runtime environments. A software system with dynamic adaptability can adapt itself to the changes of runtime environments by changing its own behavior in dynamic & flexible way. Such dynamic adaptability can be considered as a basic mechanism of software evolution. We have proposed a software model with dynamic adaptability named DAS and its description language named LEAD++. In this paper, we consider about safety issues on dynamic adaptability of component-based software systems and propose an improved DAS model named Safe DAS. The safety means that adaptable behavior of component-based software systems does not violate their consistency. To realize safe dynamic adaptability, the model supports exceptions & assertions mechanisms, atomicity & serialization of adaptable behavior and a unique mechanism named dynamic assertions that assertions can be changed dynamically.

DOI： 10.1145/602461.602504

researchmap

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

Web of Science

researchmap

Publisher：Springer  

researchmap

Other Link： http://dblp.uni-trier.de/db/conf/reflection/reflection99.html#conf/reflection/AmanoW99

Publisher：IEEE Computer Society  

researchmap

Other Link： http://dblp.uni-trier.de/db/conf/tools/tools31-1999.html#conf/tools/AmanoW99

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

A system has dynamic adaptability if it can adapt itself to dynamically changing runtime environments. As open-ended distributed systems and mobile computing systems have spread widely, the need for software with dynamic adaptability increases. We propose a model of software with dynamic adaptability and, we designed and implemented the language LEAD which constructs the model. The basic idea that we introduce the mechanism which changes procedure invocations dynamically depending on the states of runtime environments. The dynamically adaptable software based on the model is realized as a meta-level architecture, and it separets the codes of dynamic adaptability from the codes of primary subject domain in the software. LEAD provides the mechanism as a language construct and, the dynamically adaptable software in LEAD forms meta-level architecture. Using LEAD, we can realize the followings:1)the highly extensible dynamically adaptable software, and 2)the introduction of the dynamic adaptability to the existing software.

researchmap

Language：Japanese   Publisher：一般社団法人日本ソフトウェア科学会  

CiNii Books

researchmap

Publishing type：Research paper (international conference proceedings)   Publisher：World Scientific, Singapore  

researchmap

Publisher：Chapman & Hall  

researchmap

This paper reports a language-based approach to constructing adaptable applications --- application level software systems which dynamically adapt themselves to their changing runtime environments. Adaptable applications are especially indispensable to mobile distributed computing. However, such flexible applications remain more expensive to develop, maintain and port compared to their 'fixed' counterparts. Our approach is based on a language mechanism called generic procedure which enhances the modular development of adaptable applications. Using this mechanism, an application programmer c...

researchmap

Authorship：Last author   Language：Japanese   Publishing type：Research paper (scientific journal)  

DOI： 10.11309/jssst.11.3_175

CiNii Books

researchmap

Other Link： https://projects.repo.nii.ac.jp/?action=repository_uri&item_id=287616

Authorship：Lead author   Language：Japanese   Publishing type：Research paper (scientific journal)   Publisher：一般社団法人日本ソフトウェア科学会  

DOI： 10.11309/jssst.11.3_165

CiNii Books

researchmap

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

DOI： 10.1145/141937.141948

Web of Science

researchmap

Other Link： http://dblp.uni-trier.de/db/conf/oopsla/oopsla92.html#conf/oopsla/MasuharaMWY92

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

Web of Science

researchmap

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

DOI： 10.1007/3-540-55613-3_11

Web of Science

researchmap

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

Web of Science

researchmap

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

Web of Science

researchmap

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

DOI： 10.1007/BFb0057025

Web of Science

researchmap

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

DOI： 10.1007/BFb0019450

Web of Science

researchmap

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

Web of Science

researchmap

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

DOI： 10.1145/67387.67399

Web of Science

researchmap

Other Link： http://dblp.uni-trier.de/db/journals/sigplan/sigplan24.html#journals/sigplan/YonezawaW89

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

DOI： 10.1145/62084.62111

Web of Science

researchmap

Other Link： http://dblp.uni-trier.de/db/conf/oopsla/oopsla88.html#conf/oopsla/WatanabeY88

Authorship：Lead author   Language：Japanese   Publishing type：Research paper (scientific journal)   Publisher：Japanese Society for Artificial Intelligence  

A Japanese discourse understanding system is presented, which is designed to be adaptable for multiple discourse domains with small modification efforts. The system is constructed in an "object-oriented" manner so that domain-dependent/independent components are easily factored out. Dictionaries, grammatical rules, words and discourse situations are represented as objects. Two discourse domains, a railway ticket reservation domain and an electric-mail service domain, are currently used as a test bed for the system.

DOI： 10.11517/jjsai.2.2_206

CiNii Books

researchmap

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

Context-oriented programming(COP) is a programming method that enables us to define behaviors that depend on the program's execution context. We propose an implementation method of COP that does not need language extensions. Objective-C has a dynamic object system in which we can replace arbitorary methods. Harnessing such ability of the language, we construct a mechanism realizing COP. In this paper, we introduce how to construct such mechanism in Objective-C and evaluate the runtime overhead of our implementation.

CiNii Books

researchmap

Language：Japanese  

CiNii Books

researchmap

Language：Japanese  

CiNii Books

researchmap

Language：Japanese  

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：English   Publisher：一般社団法人電子情報通信学会  

We propose a method of generating realtime programs from verified models. The primary goal of this work is to provide an easy way of constructing soft realtime programs running in environments that do not provide realtime features. To realize this, the timing constraints described in a model should include properties of the runtime overhead and the generated code checks its timing constraints at runtime. In this paper, we describe how to generate plain Java/C programs from timed automata that are model-checked using UPPAAL.

CiNii Books

researchmap

Language：English   Publisher：一般社団法人電子情報通信学会  

We propose a method of generating realtime programs from verified models. The primary goal of this work is to provide an easy way of constructing soft realtime programs running in environments that do not provide realtime features. To realize this, the timing constraints described in a model should include properties of the runtime overhead and the generated code checks its timing constraints at runtime. In this paper, we describe how to generate plain Java/C programs from timed automata that are model-checked using UPPAAL.

CiNii Books

researchmap

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

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.

researchmap

Language：Japanese  

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

CiNii Books

researchmap

Language：Japanese  

本研究では、オブジェクト計算で形式的に表現できる事象を増やすために、継続オブジェクト内に保存された評価文脈を変更可能にし、継続を呼び出す時にその変更が反映される体系を提唱する。前の継続オブジェクト計算の体系では継続オブジェクト内に保存されている評価文脈内のメソッドの変更は不可能であるため、継続を呼び出して評価文脈を再利用するとき評価文脈の一部分を変更して扱いたい場合に、継続オブジェクトを作り直さなければいけなかった。これを、直接変更できるように体系を再定義し直すことで、オブジェクト計算で表現できる幅を広げる。

CiNii Books

researchmap

Language：Japanese   Publisher：一般社団法人電子情報通信学会  

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：English   Publisher：社団法人電子情報通信学会  

Computational reflection is essential to construct highly flexible and/or adaptable systems in the sense that it provides a high-level view of the structure and behavior of the sytem to itself. This paper reports our ongoing work aimed at formalizing behavioral aspects of computational reflection. Our formalization is based on the notion of implementation relations between abstract computational models. Using this approach, we can formalize full-fledged reflection without introducing reflective towers or similar infinite structures a priori. Our current contribution includes the notion of explicit metalevel diversity that provides us a way to discuss about the strength of reflectivity in formal settings.

CiNii Books

researchmap

Language：Japanese   Publisher：社団法人電子情報通信学会  

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

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

MoxaはJavaを対象とした振る舞いインターフェース記述言語であり,表明アスペクトと呼ばれる機構の導入によって仕様記述のモジュール化を促進している.本稿ではMoxaの表明アスペクトを用いた仕様記述について概観し,さらに表明アスペクトを拡張して仕様記述のモジュール化をより促進する方法について議論する.

CiNii Books

researchmap

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

We discuss a characterization of security policies to be enforced with a monitor. The monitor is a enforcement mechanism that work by observing a behavior of a program and terminating its execution if it violates a security policy being enforced. Unfortunately, the monitors is able to enforce not all of security policies in order to limit to observe for a finite behavior and not to use future informations. F.B.Schneider show that policies having the trait become to satisfy Lamport's safety property. Also, there exist Buchi automata to recognize the safety properties and he calls them security automata. Therefore we introduce automata using more information and show that these automata can enforce information flow policies with respect to noninterference.

CiNii Books

researchmap

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

We discuss a characterization of security policies to be enforced with a monitor. The monitor is a enforcement mechanism that work by observing a behavior of a program and terminating its execution if it violates a security policy being enforced. Unfortunately, the monitors is able to enforce not all of security policies in order to limit to observe for a finite behavior and not to use future informations. F.B.Schneider show that policies having the trait become to satisfy Lamport's safety property. Also, there exist Biichi automata to recognize the safety properties and he calls them security automata. Therefore we introduce automata using more information and show that these automata can enforce information flow policies with respect to noninterference.

CiNii Books

researchmap

Language：Japanese   Publisher：社団法人電子情報通信学会  

We discuss a characterization of security policies to be enforced with a monitor. The monitor is a enforcement mechanism that work by observing a behavior of a program and terminating its execution if it violates a security policy being enforced. Unfortunately, the monitors is able to enforce not all of security policies in order to limit to observe for a finite behavior and not to use future informations. F.B.Schneider show that policies having the trait become to satisfy Lamport's safety property. Also, there exist Biichi automata to recognize the safety properties and he calls them security automata. Therefore we introduce automata using more information and show that these automata can enforce information flow policies with respect to noninterference.

researchmap

Language：Japanese   Publisher：社団法人電子情報通信学会  

We discuss a characterization of security policies to be enforced with a monitor. The monitor is a enforcement mechanism that work by observing a behavior of a program and terminating its execution if it violates a security policy being enforced. Unfortunately, the monitors is able to enforce not all of security policies in order to limit to observe for a finite behavior and not to use future informations. F.B.Schneider show that policies having the trait become to satisfy Lamport's safety property. Also, there exist Biichi automata to recognize the safety properties and he calls them security automata. Therefore we introduce automata using more information and show that these automata can enforce information flow policies with respect to noninterference.

researchmap

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

We have been developing Moxa, a behavioral interface specification language tailord for Java. Moxa provides a new modularization mechanism called assertion aspect that can capture the crosscutting properties among assertions in a specification. Using this mechanism, we can modularize large and complex specification of real-world applications. In this paper, we briefly explain the design of Moxa and then discuss its extension called protocoloriented aspect description. The extension provides convenient way to describe, test and verify specifications that are described based on method invocation sequence.

CiNii Books

researchmap

Language：Japanese   Publisher：Information Processing Society of Japan (IPSJ)  

In this paper, we report the design and implementation of Moxa-a behavioral interface specification language that supports DbC (Design by Contract) based specifications. In DbC methodology, a contract arranges responsibilities between a user and a supplier of the service. This improves software quality because this makes clear who has responsibility, how to use, and what is the result of the service. With JML (Java Modeling Language), a DbC based behavioral interface specification language for Java, we can declare assertions as pre/post-conditions for each method. However, as the number of methods increases and the functionalities of services become complex, assertions for each method gets complicated. This makes it difficult to keep the consistency between assertions and methods while we are modifying them. Using Moxa, we can divide and describe assertions into several modules called assertion-aspects, when we can regard the behavior of the object(s) as the composition of some independent aspects. In JML style specification declaration, the aspects are crosscut over the assertions declared for difference methods. In this paper, we show the modularization mechanism for assertion declarations and description method provided by Moxa.

CiNii Books

researchmap

Other Link： http://id.nii.ac.jp/1001/00016611/

Language：Japanese   Publisher：Information Processing Society of Japan (IPSJ)  

In Design by Contract (DbC) facility, we explicitly specify conditions as assertions for each procedures which must hold just before/after a procedure execution, and consider them to be a contract between procedures and it's users. This makes clean who is responsible for problems of a procedure execution. The more the scale of a program grows up, the more Description of assertions based on DbC complicated, because number of assertions increases and complexity of each assertions are increased. Hence it becomes difficult to modify and/or extend programs and assertions without lose consistency between them and coherence of assertions. The reason of this problem is that we cannot modularize description of assertions independent of program structure, because in the way to describe assertions based on DbC, assertions must be embeded in the programs. So we propose an aspect-oriented modularization technique for the description of assertions based on DbC. In this technique, we think of assertion as advice, location to check the assertion as join point, and the set of them as aspect. This technique makes modularization technique for the description of assertion flexible. In this presentation, we show the implementation of Maildir Folder Service Provider we developed, which manages E-mail messages in Java, and we describe a test of this implementation using Java Modeling Language (JML) which extends java to be able to describe assertions base on DbC. Next, we show the problems for increasing of description of assertions in the test process, and propose aspect-oriented modularization technique for description of assertions. And then, we compare this technique with JML and show this method is more preferable. And finally, we show a method to generate state transition models from a modularized description of assertions.

CiNii Books

researchmap

Publisher：Information Processing Society of Japan (IPSJ)  

In Design by Contract (DbC) facility, we explicitly specify conditions as assertions for each procedures which must hold just before/after a procedure execution, and consider them to be a contract between procedures and it's users. This makes clean who is responsible for problems of a procedure execution. The more the scale of a program grows up, the more Description of assertions based on DbC complicated, because number of assertions increases and complexity of each assertions are increased. Hence it becomes difficult to modify and/or extend programs and assertions without lose consistency between them and coherence of assertions. The reason of this problem is that we cannot modularize description of assertions independent of program structure, because in the way to describe assertions based on DbC, assertions must be embeded in the programs. So we propose an aspect-oriented modularization technique for the description of assertions based on DbC. In this technique, we think of assertion as advice, location to check the assertion as join point, and the set of them as aspect. This technique makes modularization technique for the description of assertion flexible. In this presentatio

researchmap

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

CiNii Books

researchmap

Language：Japanese   Publisher：Information Processing Society of Japan (IPSJ)  

CiNii Books

researchmap

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

CiNii Books

researchmap

Publisher：Japan Society for Software Science and Technology  

It is known that the class of security policies enforced by a simple execution monitoring (EM) is included in the class of safety properties. The goal of this work is the characterization of enforceable policies using mechanisms in EM augmented with information obtained by program analysis. In this paper, we focus on confidentiality and availability enforced by the augmented EM.

DOI： 10.11309/jssstconference.21.0.67.0

researchmap

Publisher：Japan Society for Software Science and Technology  

Design by Contract is a technique to design correct softwares by specifying constraints as assertions that hold before and after a software component executes.By using this approach, the more assertion we added, the more complicated the system will be.We found that it is hard to preserve consistency on this way.To solve this problem, we introduce Aspect-Oriented modularization method for specification language.This is the method which split a large specification to some partial parts, which we take as aspect.Then we propose the translation method of the partial parts, aspect, to the State-transition model.

DOI： 10.11309/jssstconference.21.0.24.0

researchmap

Language：Japanese   Publisher：一般社団法人日本ソフトウェア科学会  

CiNii Books

researchmap

Language：Japanese   Publisher：Information Processing Society of Japan (IPSJ)  

Mobile code has been regarded as a convenient abstraction mechanism to construct flexible/evolvable distributed computing systems. It has now gained prominence, mainly due to the current shift from stationary to mobile/ubiquitous computing environment. Although designing a system using mobile code is appealing, its deployment is still a security risk. Further, a system using mobile code is inherently dynamic; we need an extensible/adaptable security model. In this talk, we first claim that application-dependent and special-purpose security policies are increasingly important especially for modern distributed computing environment. Then we present a set of techniques that may be used to enforce such policies on mobile objects (Java classes) . The main technique is a load-time bytecode modification that enforces user-defined policies via monitored execution. The policies are written in a language called Polaris, which is basically a finite process language enhanced to deal with data-dependencies among variables. Use of data-dependencies reduced the cost of monitoring. As an example, we show a code portion from our extensible e-mail client system. Web site of this project: http://www.psg.cs.titech.ac.jp/sc/

CiNii Books

researchmap

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

Mobile code has been regarded as a convenient abstraction mechanism to construct flexible/evolvable distributed computing systems. It has now gained prominence, mainly due to the current shift from stationary to mobile/ubiquitous computing environment. Although designing a system using mobile code is appealing, its deployment is still a security risk. Further, a system using mobile code is inherently dynamic; we need an extensible/adaptable security model. In this talk, we first claim that application-dependent and special-purpose security policies are increasingly important especially for modern distributed computing environment. Then we present a set of techniques that may be used to enforce such policies on mobile objects (Java classes) . The main technique is a load-time bytecode modification that enforces user-defined policies via monitored execution. The policies are written in a language called Polaris, which is basically a finite process language enhanced to deal with data-dependencies among variables. Use of data-dependencies reduced the cost of monitoring. As an example, we show a code portion from our extensible e-mail client system. Web site of this project: http://www.

researchmap

Publisher：Japan Society for Software Science and Technology  

Aspect-oriented languages support clear separation of code which crosscuts two or more classes. We believe it is possible to combine independently developed aspects safely, if each aspect is designed according to certain rules. As first step for finding out and verifying such rules, we describe how to verify rules for safely composable mixins. The notion of "Design by Contract" and "behavioral subtyping" are used for description and verification of the rules.

DOI： 10.11309/jssstconference.19.0.3E3.0

researchmap

Language：Japanese   Publisher：共立出版  

CiNii Books

researchmap

Language：Japanese   Publisher：Information Processing Society of Japan (IPSJ)  

We focus on the problems in the development of CORBA applications : interface mismatches which often take place in cross-platform development, and complicated development procedure which consists of generating stubs and skeletons and incorporating them into applications. We propose a solution of these problems using the Interface Repository and refletive programming languages. We inspect the abilities of reflective languages to realize this solution, especially generation and modification of programs and modification of the behavior of the languages in referring undefined names.

CiNii Books

researchmap

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

We focus on the problems in the development of CORBA applications : interface mismatches which often take place in cross-platform development, and complicated development procedure which consists of generating stubs and skeletons and incorporating them into applications. We propose a solution of these problems using the Interface Repository and refletive programming languages. We inspect the abilities of reflective languages to realize this solution, especially generation and modification of programs and modification of the behavior of the languages in referring undefined names.

researchmap

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

A reflective system can understand/compute its structure and behavior at run time. Giving the facility of reflection to OS or programming languages, it is possible to construct the advanced and complex systems, like mobile computing systems of distributed systems, with more systematic manner. Practically, the programmer might want to apply several extensions to the language simultaneously. But, there might be some semantical conflicts between these extensions. In this article, we propose a framework to avid the conflicts. We provide a modular implementation of a reflective programming language based on monad transformers, and made its internal dependency of each component clear. And then, we propose a concrete mechanism to help a user who want to extend a language know enough informations to avoid possible conflicts.

researchmap

Language：Japanese   Publisher：Information Processing Society of Japan (IPSJ)  

A reflective system can understand/compute its structure and behavior at run time. Giving the facility of reflection to OS or programming languages, it is possible to construct the advanced and complex systems, like mobile computing systems of distributed systems, with more systematic manner. Practically, the programmer might want to apply several extensions to the language simultaneously. But, there might be some semantical conflicts between these extensions. In this article, we propose a framework to avid the conflicts. We provide a modular implementation of a reflective programming language based on monad transformers, and made its internal dependency of each component clear. And then, we propose a concrete mechanism to help a user who want to extend a language know enough informations to avoid possible conflicts.

CiNii Books

researchmap

Language：Japanese   Publisher：Information Processing Society of Japan (IPSJ)  

Usually, a metalevel is designed for a specific application domain, especially when the metalevel is dedicated for extensibility because details of the extensibility are very application specific issues. The aim of this study is to extract characteristics common to all metalevel architectures and to establish a method for structuring a metalevel using the characteristics for extensibility of the metalevel. The methodology eases metalevel designs and its extensions because it is applicable to most application domains since they are not depending to specific domains. The metalevel should be constructed by multiple modules organized as stable and open structures. We propose that the methodology structuring a metalevel by baselevel syntax and sticking semantic modules to the syntactic elements. Baselevel syntax is common characteristics for all metalevels since they have a defintion of the baselevel and it contains the syntax definition. Therefore the structuring method is applicable to most metalevels. The modules interact with single assignment attributes defined for each edge of baselevel syntax tress. Since the attributes can be defined as many as required, multiple semantic modules can be sticked to on syntactic element without any interference. Consequently we can introduce new modules for extensions easily. This paper explains the methodology by examples including lambda calculus and LR parser generator.

CiNii Books

researchmap

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

Usually, a metalevel is designed for a specific application domain, especially when the metalevel is dedicated for extensibility because details of the extensibility are very application specific issues. The aim of this study is to extract characteristics common to all metalevel architectures and to establish a method for structuring a metalevel using the characteristics for extensibility of the metalevel. The methodology eases metalevel designs and its extensions because it is applicable to most application domains since they are not depending to specific domains. The metalevel should be constructed by multiple modules organized as stable and open structures. We propose that the methodology structuring a metalevel by baselevel syntax and sticking semantic modules to the syntactic elements. Baselevel syntax is common characteristics for all metalevels since they have a defintion of the baselevel and it contains the syntax definition. Therefore the structuring method is applicable to most metalevels. The modules interact with single assignment attributes defined for each edge of baselevel syntax tress. Since the attributes can be defined as many as required, multiple semantic module

researchmap

Language：Japanese   Publisher：Information Processing Society of Japan (IPSJ)  

CiNii Books

researchmap

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

自己反映的なプログラミング言語は 言語自身を計算の対象として扱うことが可能な言語システムである.言語の実装レベルに相当する記述をメタレベルとして実際の計算に関する記述と分離することによって 実行時の状況に応じた動的な言語の拡張を 再利用可能なモジュールとして提供することが可能な枠組みであり 並列計算機や 分散計算機環境におけるアプリケーションの記述を簡潔におこなうことができる.しかし 自己反映的な言語を実装する場合 言語の内部構造をユーザーにどのようにして提示するかの選択によって その言語が提供する拡張性と実行効率とのトレードオフが生じる.実際の自己反映的な言語では 並列計算などの特定の用途に限った自己反映計算を提供する言語として設計されることが多く 実験的なものを除いては汎用的な用途に適した言語といけるようなものはない.本稿では 用途を限定しない自己反映的な言語の効率的な実装方法を提案したい.そこでそのような実装方法を提供するための枠組みとして Monad-Transformerをもちいた.本稿ではまず 自己反映的な言語のいくつかの形式を 拡張可能な機能ごとに独立したモジュールの組として定義するための枠組みを示し 次にプログラマーがプログラムの各局面に応じ 必要な拡張機能と実行効率を考慮した言語の実装形態を随時選択するためのインターフェイスを提案する.最後に実際の言語システムの構築における問題点などに関する考察をおこなう.Reflective programming languages are languages which enable user programs to run at the defining language level (meta-level), and act as a part of the interpreter. So reflective languages can provide high extensibility. But in fact, in most of implementations of such a language, the given way of extension is not flexible enough. Because in the traditional methodology of defining reflective language is structuring the language as a meta-circular interpreter, so if we try to provide extensibility as possible. The performance to execute such programs are too low to build practical applications. Some reflective systems restrict extensibility of the language, and solve meta-level computations at compile-time. But, if what we can do at meta-level is limited hardly, or extensions have effect on only statically, there is less advantage of reflection about extension. In this paper, we propose a modular implementation technique of reflective languages. To provide the mechanism, we define some language building-blocks. And then we build a meta-continuation based reflective language as an interpreter and a compiler for the normal (non-reflective) language. Our goal is designing interfaces to let the programmer possible to select the implementation of the reflective language and make user to be able to specify the language for the purpose of each program-pieces. So we conclude what is the most efficient combination of language modules for some domain.

researchmap

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

In this paper, we show the usefulness of the capabilities of a reflective programming language in developing CORBA applications. We show two examples. One can make application development process in CORBA simpler and easier. Stubs and skeletons in CORBA applications can be generated and incorporated at runtime with the use of reflection. Another can make programming with complicated CORBA APIs simpler and easier, too. We can reduce programming efforts of the deferred synchronous invocation API and the DynAny API.

CiNii Books

researchmap

Language：Japanese   Publisher：一般社団法人電子情報通信学会  

CiNii Books

researchmap

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

researchmap

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

CiNii Books

researchmap

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

CiNii Books

researchmap

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

CiNii Books

researchmap

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

CiNii Books

researchmap

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

CiNii Books

researchmap

Language：Japanese   Publisher：一般社団法人電子情報通信学会  

This paper presents a formal specification in rewriting logic of a representative subset of GAEA, in the Prolog traditional with novel features for reflection and concurrency, based on a new software methodology called organic programming. The syntax and the semantics of GAEA were designed to be a superset of Prolog. However, there are many extra features for manipulating cell structures, multi-threading of processes, cell variables for thread communication, and so on. Thanks of those new features, we can easily construct and execute concurrent reflective systems.

CiNii Books

researchmap

Language：Japanese   Publisher：Information Processing Society of Japan (IPSJ)  

A system has dynamic adaptability if it can adapt itself to dynamically changing runtime environments. As open-ended distributed systems and mobile computing systems have spread widely, the need for software with dynamic adaptability increases. We propose a model of software with dynamic adaptability and, we designed and implemented the language LEAD which constructs the model. The basic idea that we introduce the mechanism which changes procedure invocations dynamically depending on the states of runtime environments. The dynamically adaptable software based on the model is realized as a meta-level architecture, and it separets the codes of dynamic adaptability from the codes of primary subject domain in the software. LEAD provides the mechanism as a language construct and, the dynamically adaptable software in LEAD forms meta-level architecture. Using LEAD, we can realize the followings:1)the highly extensible dynamically adaptable software, and 2)the introduction of the dynamic adaptability to the existing software.

CiNii Books

researchmap

Other Link： http://id.nii.ac.jp/1001/00012969/

Language：Japanese   Publisher：一般社団法人電子情報通信学会  

Reflective programming Languages allows user's progrms to customize the behavior of the language. To develop practical application programs, users desire to reuse metalevel-difinisions that had been defined before. But it is difficult for designers to make the definitions these can be reused, because they may cause conflicts mutally. This paper proposes an specific example of a reflective language which is build modularly by monad-transformer, an show that it is easy for the language to specify the conflicts and avoid them, and gives conclusions to applly the experience for general case.

CiNii Books

researchmap

Language：Japanese   Publisher：一般社団法人日本ソフトウェア科学会  

CiNii Books

researchmap

Language：Japanese   Publisher：Information Processing Society of Japan (IPSJ)  

CiNii Books

researchmap

Language：Japanese   Publisher：一般社団法人電子情報通信学会  

モバイルエージェントやJavaなどのWebページ記述用言語に代表される移動可能プログラムをいつでもどこでも計算機を使用可能とするモバイルコンピューティング環境と組み合わせることによって, 計算機の可能性は飛躍的に向上する. 本稿では, 移動可能プログラムと移動可能プログラムをモバイルコンピューティング環境上で実行するために必要となる適応可能なソフトウェアアーキテクチャに関して紹介する.

CiNii Books

researchmap

Language：Japanese   Publisher：北陸先端科学技術大学院大学  

CiNii Books

researchmap

Language：Japanese   Publisher：一般社団法人電子情報通信学会  

We propose a new method of designing/implementing metalevel architectures for extensible programming languages. Using our method, we construct a language processor (interpreter) by composing resusable metaleval parts. Thanks to the design principle (called Interpreter Passing Style) of these parts, we can freely add/replace a part without affecting other parts of the interpreter.

CiNii Books

researchmap

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

The question we are considering is whether a representation-independent model of computational reflection exists. We use abstract rewriting systems as general operational models of computation. We define reflection based on the notion of implementation morphisms on ARSs. This paper presents our preliminary results.

CiNii Books

researchmap

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

オブジェクト指向プログラミングにおけるソフトウェア開発において、クラスライブラリ、およびそれを有効に利用するための開発環境の役割は大変重要である。クラスライブラリを含めた開発環境を単なるソースコードのデータベースとしてだけ捉えるのではなく、情報を整理し、資産として再利用可能な形で蓄積してゆくための一手段として捉える必要がある。しかし、その一方でクラスライブラリを構成するための標準的な方法は示されておらず、設計者それぞれ固有のモデルに委ねられている。そのため利用者は、プログラミング言語の習得のみならず、各設計者によって作成されたクラスライブラリの理解をも強いられる。加えて、クラスライブラリは肥大化するばかりで、利用者の負担は増える一方である。ここに初心者がオブジェクト指向プログラミングになじめない理由の一つがある。そのためにも、クラスライブラリが備えるべき標準的な性質を設計者、利用者ともに認知する必要がある。本稿では、問題領域に特化しないという意味での汎用のクラスライブラリ、および、プログラミング言語に特化しないという意味での汎用のクラスライブラリを構成するための方法について考察する。

CiNii Books

researchmap

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

近年の技術革新は電子装置の小型化、高性能化をもたらし、その製造技術の進歩はそれらの安価な実現を可能にした。またネットワークはパソコン通信などを通じて急速に個人の生活空間に浸透しつつある。小型化された携帯可能な電子装置とネットワーク、この2つの技術の融合により新しいコンピューティング環境、コンピューティングスタイルが生まれようとしている。このように移動可能な小型計算機をネットワークに接続し、分散環境と融合させた計算機環境を移動計算機環境という。移動計算機環境では移動による計算機を取り巻く環境の動的変化、計算機資源の制約等がシステムレベルの透過性実現を困難にしている。本研究ではこのような環境においてシステムレベルの透過性を実現する枠組として有効なメタレベルアーキテクチャで構成される言語を提案する。

CiNii Books

researchmap

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

自己反映計算とは、通常の計算対象だけでなく計算を行なっている自己をも対象として計算を行なう、という概念である。自己反映的プログラミング言語とは、自己(動作中のプログラムや処理系の状態など)をその言語自身の枠組の中で扱うことができるようなプログラミング言語のことである。自己反映的なシステムでは、自己の構成、状態を動的に変更することが可能である。従って、自己反映的プログラミング言語は問題領域に合わせて自分自身をカスタマイズでき、柔軟なソフトウェアの構築に有用であることが認識されている。また、プログラム自体を扱う部分(メタレベル)と、問題を扱う部分(ベースレベル)に分けるという意味でモジュール化の促進を可能とする。本稿では、手続き的自己反映計算(ベースレベルを何らかのプログラムとすると、メタレベルをそのプログラムを実行するインタプリタとする枠組)において、モジュール化という側面を重視し、メタレベルの再利用性を考慮した自己反映的プログラミング言語のアーキテクチャを提案する。

CiNii Books

researchmap

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

分散計算環境における大域的ガベージコレクションの一手法を提案する.本方式はリファレンスカウント方式とマーキング方式を併用したアルゴリズムを採用し,以下のような特長を持つ:(1)循環する参照を含むすべてのゴミを回収できる.(2)アプリケーションプログラムと並行に動作する.(3)比較的オーバーヘッドの高いマーキングフェーズの稼働率を低くおさえている.(4)リファレンス,構報,マーキング,終了判定のメッセージに重みを用いて,メッセージ数を減少させている.(5)集中制御を必要としない.本方式によるGCをCM-5,nCUBE/2上に実装し,他のアルゴリズムとの比較も行った.

CiNii Books

researchmap

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

移動計算機を無線ネットワークを用いて分散環境と接続した移動計算機環境におけるアプリケーションは、メモリのサイズ、バッテリの量、ネットワークのバンド幅などの制約を考慮して実行する必要がある。そのため、アプリケーションやOSの構成力環境に応じて柔軟に変化しなければならない。本稿では、移動計算機環境に適した柔軟なソフトウェアの構築法の開発をめざすParsifalプロジェクトにおける柔軟なソフトウエアの構築法に関する概要を述べる。

CiNii Books

researchmap

Language：Japanese   Publisher：一般社団法人電子情報通信学会  

We propose a new implementation scheme for object-oriented concurrent Ianguages.In our scheme the execution of concurrent objects is modeled as a concurrent term rewriting.Rewriting terms that represent concurrent objects is realized by a system of interconnected graph rewriting machines.Soundness of our system execution is showed using a rewriting logic for object-oriented concurrent languages.

CiNii Books

researchmap

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

The goal of this work is to provide a clear and general description framework forcomputational reflection and its related concepts(such as introspection,reflective tower,partial computation,and so on).This paper presents our first attempt to construct sucna framework based on the notion of implementation on abstract rewriting systems.

CiNii Books

researchmap

Language：Japanese   Publisher：北陸先端科学技術大学院大学  

CiNii Books

researchmap

Language：Japanese   Publisher：北陸先端科学技術大学院大学  

CiNii Books

researchmap

researchmap

Language：Japanese   Publishing type：Book review, literature introduction, etc.   Publisher：社団法人人工知能学会  

DOI： 10.11517/jjsai.2.4_536

CiNii Books

researchmap

Language：Japanese   Publishing type：Book review, literature introduction, etc.   Publisher：情報処理学会  

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap