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.