
(理論面の)対象 | 圏論を応用して推論への異なるアプローチを統一することを目的に、様々な論理体系を研究・比較。 |
(理論面の)目標 | ソフトウェアシステムの仕様記述や検証など、形式手法の発展に数学的基礎を提供する。 |
ここまでの成果/重要な発見 | 再構成可能なソフトウェアシステムの効率的な開発をサポートする論理基盤を構築。これらのシステムは、外部または内部の刺激に応答して動的に構成を調整するメカニズムを特徴とする。 |
これからの目標/現在取り組んでいる目標 | 再構成可能システムをモデル化するために使用される論理システムの特徴づけを与える定理を確立する。 |
応用上の成果/目標 | ソフトウェアシステムの記述と推論のための仕様言語と定理証明器の開発。 |
さらなる発展の可能性・方向性 | 今後の研究の方向性の一つは、量子プログラムの仕様化と検証の基盤となる量子モデル理論の開発である。 |
My research interests are rooted within algebraic specification, oneof the most promising aproach to formal methods assisting the developing of software systems at several stages such as design, specification and formal verification. Algebraic specification and programming languages are rigorously based on logic, which amounts to the existence of a logical system underlying the language such that each language feature and construction can be expressed as a mathematical entity of the underlying logic.
The current goal of my research is to develop mathematical and logical structures supporting the efficient development of correct reconfigurable software systems, i.e. systems with reconfigurable mechanisms managing the dynamic evolution of their configurations in response to external stimuli or internal performance measures. A typical example of reconfigurable system is given by the cloud-based applications that flexibly react to client demands by allocating, for example, new server units to meet higher rates of service requests. The model implemented over the cloud is pay-per-usage, which means that the users will pay only for using the services. Therefore, the cloud service providers have to maintain a certain level of quality of service to keep up the reputation.
Reconfigurable systems are safety- and security-critical systems with strong qualitative requirements, and consequently, formal verification is needed.
キーワード | Logic, Formal Methods, Category Theory |
---|---|
部門 | オーストラリア分室 |
リンク | ホームページ Constructor-based Inductive Theorem Prover (CITP) |