Communication software engineering based on formal methods

反应系统的质量对工业、公共安全和安保至关重要。测试和验证活动占反应性系统开发成本的很大比例。重要的是要开发新的方法、技术，并尽可能增强在构成反应系统生命周期的各种活动中使用的现有方法。我研究的目的是提高最终产品的质量，降低其开发成本。最终的解决方案是通过构造来获得系统的正确性，这意味着基于形式化方法的规范推导和后续开发步骤的自动化。不幸的是，这个解决方案还不可用。在此之前，处理系统质量的唯一方法是进行一些部分建模、部分验证和验证(使用抽象和推理进行部分证明)和测试。更具体地说，我的研究目的是改进跨异构网络的可靠服务的开发。需要在高级网络平台上快速开发服务。服务提供商和网络运营商面临的主要挑战是快速提供高质量的服务。正在进行的研究的目的是提供一种服务创建、规范方法和原型工具，帮助设计人员在其环境的背景下创建、规范、验证、实施和测试新服务。拟议的方法将以正式技术的使用为基础。我认为，形式化技术是故障检测、故障避免和开发过程自动化的关键。众所周知，在开发过程中较早检测到的设计故障的成本将低于在维护步骤中检测到的相同故障的成本。出于这些原因，我的研究将集中在复杂系统的规格说明、设计和测试步骤上。“质量”这个关键词是连接我所有研究项目的纽带。

The quality of reactive systems is of prime importance to industry, public safety and security. Testing and validation activities represent a substantial percentage of the development costs of reactive systems. It is important to develop new methods, techniques and enhance, as much as possible, the existing approaches that are used in various activities that compose reactive systems' life cycle. The objective of my research is to enhance the quality of end-product and to reduce their development costs. The ultimate solution is to obtain the correctness of systems by construction, which means the derivation of specifications based on formal methods and the automation of subsequent development steps. Unfortunately, this solution is not yet available. Until then, the only way to deal with the quality of systems is to perform some partial modeling, partial validation and verification (partial proof using abstraction and inference) and testing.  More specifically, the aim of my research is to improve the development of reliable services over heterogeneous networks. There is a need for rapid development of services over advanced network platforms. The main challenge for service providers and network operators is the rapid provisioning of high quality services. The aim of the on-going research is to provide a service creation, specification methodology and prototype tools that assist designers with the creation, specification, validation, implementation and testing of new services in the context of their environment. The proposed methodologies will be based on the use of formal techniques. I believe that formal techniques are the key for fault detection, fault avoidance and automation of the development process. It is well known that design faults that are detected earlier in the development process will cost less than the same faults detected at the maintenance step. For these reasons, my research will focus on specification, design and test steps of complex systems. The keyword "Quality" is the link between all my research projects.