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.