1. Full name: Nguyen Trinh Dong                                              2. Sex: Male     

3. Date of birth: 12/07/1974                                                       4. Place of  birth:  Hai Phong     

5. Admission decision number: 3613/QĐ-SĐH  Dated 22/10/2009

6. Changes in academic process:

7. Official thesis title:

Methods for modeling and verifying of component-based real-time systems

8. Major: Software Engineering                                                  9. Code: 62.48.01.03     

10. Supervisors: Dr. Dang Van Hung and Assoc. Prof. Truong Anh Hoang

11. Summary of the new findings of the thesis:

First, the dissertation proposes an extension of the PECOS (PErvasive COmponent Systems) model to apply for real-time components. This model can be used to analyze various factors of functional and non-functional in components. This model is divided into two parts, the passive part, and the active part. The passive part is considered as a repository of real-time components that is able to provide components meeting every system requirement. The active part plays the role of interacting with an environment, receiving requests from the environment, and invoking services from the passive part to process, then retrieving the results back to the environment. Besides, the model is divided into two parts with the aim of reducing the complexity of the system due to the system development based-on divide-and-conquer strategy and to control parallel processes in systems that based on this model. The model also allows the processes of components in both parts to implement in parallel. In addition, in order to accurately analyze interactions in component-based real-time systems, the dissertation also proposes an interaction protocol with timing constraints and resource constraints by specifying the order of services in components based on regular expression over the distributed alphabet and modeling the behavior sequences of the system environment by timed automata and priced/weighted automata. The dissertation also proposes algorithms for checking the conformance of behavior sequences of environments to the interaction protocols, over both functional and non-functional aspects, of components. The conformance of an environment to a protocol of a component also indicates the effective utilizing system resources that the environment provides to the component.

Second, the dissertation proposes an extension of component interface theory becomes the real-time interface theory for specification and modeling of component-based real-time systems. A real-time interface is a tuple of three elements including input variables, output variables, and a relation among input variables and output variables and time constraints on the relation. This relation is described by a first-order-logic formula to assert that if an environment assigns a set of values ​​that satisfies conditions over the input variables of an interface, then the interface will ensure that the output results will meet the requirements of the system environment for timing constraints. With this approach, the sequential behaviors and functionalities of a software component are specified more concisely, plainly and elaborately. Since sequential behaviors of a real-time component interface are infinite, the thesis uses duration automata to finitely represent the behavior sequences of a real-time interface and its environments. This thesis uses duration automata because of its advantages in specifying and modeling worth case execution time (WCET) and at least time (i.e. best case execution time) of a behavior in a component interface. In this contribution, the dissertation also takes into account the using of interfaces by its environment depending on the pluggability of an environment to a component interface. Therefore, the using of real-time interfaces with the relation among input and output variables is an effective method to verify and validate component-based real-time systems.

Third, the thesis proposed a technique that model and verify component-based real-time systems by timed contracts and timed contracts with resource constraints based on both approaches correctness-by-construction and design-by-contract. This technique allows elaborately specifying real-time components in the method level in which includes input/output variables as well as constraints on input/output variables. In addition, this technique also explicitly indicates what kind of resources and methods that software components need to implement system requirements and which services that components provide to their environments with how does it cost? This technique also allows specifying the invariant elements, resource invariant elements. In particular, this method applies the interaction protocol, which is mentioned in the first contribution, to specify the interaction of services among software components and its environments. Especially, in a software component, the execution order of methods are represented by a real-time regular expression that has resource constraints. When the environment wants to use services from a software component, the environment must provide adequately resources for the services in the component, and the environment must conform to the order in which software services are called. Through this adherence, the software component will ensure the quality of the services it provides. Thus, by this technique, a component-based real-time system is developed incrementally by composing timed contracts. Hence, the elements in this system are fully analyzed and evaluated in both functional and non-functional aspects. To be able to implement in practice, the thesis also proposes a template real-time specification language that unifies real-time specification languages with fully functional and non-functional specification features. Based on this technique, component-based real-time systems are fully qualified and specification of components in terms of timed contracts are used as the basis for improving software quality.

12. Practical applicability, if any:

The main result of this dissertation can be applied to develop large-scale and complicated component-based real-time systems.

13. Further research directions, if any:

Applying the theories for embedded systems, robot, multi-agent systems, etc. Developing a tool to support for analyzing and estimating two functional and non-functional aspects of component-based real-time systems.

14. Thesis-related publications:

Nguyen Trinh Dong, Dang Van Hung and Truong Anh Hoang (2011), “Real-Time Relational Interface Behavior Modeling and Specification”, KSE 2011-Third International Conference on Knowledge and Systems Engineering, pages 112-119.

 Nguyen Trinh Dong (2015), “Memory Resource Estimation of Component-Based Systems”, 4th International Conference, ICCASA 2015, Vung Tau, Vietnam, November 26-27, pages 73-82.

 Dang Van Hung, Nguyen Trinh Dong and Truong Anh Hoang (2017), "A Model for Real-timed Concurrent Interaction            Protocols in Component Interfaces", VNU Journal of Science: Computer Science and Communication Engineering, vol.33, no.1, pages 8-15.

 Nguyen Trinh Dong, Dang Van Hung, Truong Anh Hoang (2017), “A formal contract-based model for component-based real-time systems”, The 4th National Foundation for Science and Technology Development Conference on Information and Computer Science (NICS 2017), pages 230-235.

Nguyen Trinh Dong (2017), “A General Model for Quality Analyzing of Functional and Non-functional Features in Real-Time Systems”, The 6th Conference on Information Technology and Its application (CITA 2017), pages 15-22.