This study addresses the issue of communication link interruptions in train platoon control under the complex operating environment of high-speed railways. An adaptive trajectory tracking control approach based on a finite-time sliding mode is proposed under jointly connected switching topologies. The proposed framework ensures platoon consensus under jointly connected switching topologies, where the leader’s information need not reach all followers in each topology but only collectively over a finite interval, thus relaxing connectivity requirements and enhancing practicality. Within this framework, the sliding surface is designed to incorporate relative error signals determined by the communication topology, and an adaptive mechanism is employed to effectively handle unknown external disturbances without requiring prior knowledge of their bounds or derivatives. Simulation results demonstrate that, compared with MPC and non-adaptive approaches, the proposed strategy reduces position errors by approximately 80% and velocity errors by around 40%, significantly improving platoon tracking accuracy. Furthermore, simulations under both periodic and random topology switching indicate that periodic switching achieves performance closer to that of a fully connected topology, further enhancing trajectory tracking effectiveness.

System-level design, and dependability prediction of safety-critical systems demand integration of architectural and analysis artifacts in a single development environment. Hybrid systems, with mutual dependencies and extensive interactions between the control portion and its physical environment, further intensify this need. Architecture Analysis and Design Language (AADL) is a model-based engineering language for the architectural design and analysis of embedded control systems. Core AADL has been extended with sublanguages for modeling and analysis of discrete behavior of the control portion, but not for continuous behavior of the physical environment. In a previous work, we have introduced Hybrid Annex for continuous behavior modeling as part of initial findings of an ongoing research effort on fulfilling the need for integrated modeling of the computing system along with its physical environment. In this article, we first detail complete structure of the Hybrid Annex along with appropriate examples for each section. Then, we present formal semantics of the synchronous subset of AADL models annotated with Hybrid Annex specifications using Hybrid Communicating Sequential Processes (HCSP). Formal semantics are used to verify correctness of AADL models (with Hybrid Annex specifications) using Hybrid Hoare Logic (HHL). A case study on a realistically-scaled automatic cruise control system is provided to demonstrate modeling and verification of hybrid systems using AADL with the proposed extension.

Train platoon improves railway efficiency by coordinating train speeds and inter-train distances. However, actuator delays pose a major challenge to maintaining safe dynamic spacing. This study develops a safety-oriented framework that integrates hybrid control with reachable set estimation to explicitly compute the minimum safe separation under actuator delays. A unified modelling strategy is proposed that incorporates actuator delays together with real-time acceleration disturbances of the leading train. By using forward reachable set analysis, the effect of actuator delays on position errors is estimated and incorporated into the controller to compensate for such delays, thereby improving the safety and robustness of train platoon tracking. The influence of actuator delays on safety during emergency braking scenarios is evaluated through simulation and field experiments. The results show that the forward reachable set of position errors expands as the actuator delays increase. The adoption of controller can reduce the influence of actuator delay on the safety margin by approximately 60%. Compared with the method of eliminating delay using the Lyapunov-Krasovskii functional method, the proposed method ensures the safety of the tracking distance of the train platoon.

The Architecture Analysis Design Language (AADL) is an architecture description language for design of cyber-physical systems–machines controlled by software. The AADL standard, SAE International AS5506D, describes Run-Time Services (RTS) to be provided to execute AADL models in accordance with semantics defined by the standard. The RTS of primary concern are transport services and timing services. Although, the study presented in [1] sets a foundation for the formal semantics of AADL, but without modeling time. This paper extends and simplifies this formalization using a modal logic defined by a Kripke structure, to explicitly include time. The RTS defined in the AADL standard are also expanded to support reactive state-transition machines of the Behavior Specification annex standard language (BA) and its closely-related, formally-defined counterpart, the Behavior Language for Embedded Systems with Software (BLESS). An example of AADL RTS with time, implemented by the High Assurance Modeling and Rapid Engineering for Embedded Systems (HAMR) for state-transition machine behavior written in BLESS, is also presented.

Safety-critical cyber-physical systems require evidence they are indeed safe. In practice, such evidence is results of system tests. Unfortunately, tests can only demonstrate the presence of software errors, not their absence, and can practically cover a tiny fraction of system state space. Valiant efforts to formally verify program correctness have either been excruciatingly difficult (theorem proving) or incomplete (static analysis, model checking, SAT or SMT solving). The BLESS Methodology was created specifically for engineers in industry to formally verify software controlling machines. The BLESS Methodology transforms programs that control machines, annotated with assertions to form proof outlines, into deductive proofs that every possible program execution will conform to its specification. To the extent that cyber-physical system specifications have been validated to express system safety and performance, a deductive proof can be a convincing argument to a person of program correctness. This paper uses a simple safety-critical system to argue that behavior correctness proof under the BLESS Methodology is a convincing verification artifact in addition to customary testing.

The Architecture Analysis and Design Language (AADL) is a SAE standard for modeling both hardware and software architecture of embedded systems. Widely embraced by stakeholders in critical real-time embedded systems, the AADL standard is used to address a large set of concerns including performances (latency, schedulability), safety, and security. The ADEPT workshop aims to present and report on current projects in the field of design, implementation, and verification of critical real-time embedded systems where AADL is a first-citizen technology. This article is a summary of the second edition of the workshop in 2023.

The Internet of Medical Things (IoMT) represents a specialized domain within the Internet of Things, focusing on medical devices that require regulatory approval to ensure patient safety. Trusted composition of IoMT systems aims to ensure high assurance of the entire composed system, despite potential variability in the assurance levels of individual components. Achieving this trustworthiness in IoMT systems, especially when using less-assured, commercial, off-the-shelf networks like Ethernet and WiFi, presents a significant challenge. To address this challenge, this paper advocates a systematic approach that leverages the Architecture Analysis & Design Language (AADL) along with Behavior Language for Embedded Systems with Software (BLESS) specification and implementation. This approach aims to provide high assurance on critical components through formal verification, while using less-assured components in a manner that maintains overall system determinism and reliability. A clinical case study involving an automated opioid infusion monitoring IoMT system is presented to illustrate the application of the proposed approach. Through this case study, the effectiveness of the systemic approach in achieving trusted composition of heterogeneous medical devices over less-assured networks is demonstrated.

Trajectory prediction of the train ahead is vital for deciding the minimum safe distance for train separation. An important research challenge, in this regard, is how to effectively and accurately estimate the trajectory of the train ahead using spatiotemporal approaches with train operating data. In this paper, we present a novel hybrid model for predicting train trajectories by integrating Long Short-Term Memory (LSTM) and Kalman Filter (KF). In the proposed hybrid LSTM-KF model, the LSTM model is used to analyze time series data and discover the long-term dependencies of train trajectory data, which can be assumed as observation data for the KF model. The KF model can combine train dynamics mechanism to extract local features of train operation data, so as to smooth the train trajectory predicted by LSTM model. A novel on-the-fly algorithm is devised for efficient realization of the proposed LSTM-KF model. Experiments are carried out using the train data collected from Chengdu Metro Line 8. The results indicate that our hybrid LSTM-KF model has greatly improved the accuracy of long-term train trajectory prediction.

Purpose This paper explores the convergence of Education 4.0 and Industry 4.0 and presents a Twin Peaks model for their seamless integration. Design/methodology/approach A high-level literature review is conducted to identify and discuss the important challenges and opportunities offered by both Education 4.0 and Industry 4.0. A novel Twin Peaks model is devised for the convergence of these domains and to cope with the challenges effectively. Findings The proposed Twin Peak model for the convergence of Education 4.0 and Industry 4.0 suggests that the development of these two domains is interdependent. It emphasizes ethical considerations, inclusivity and understanding the concerns of stakeholders from both education and industry. We have also explained how continuous incremental adaptation within the proposed Twin Peaks model might assist in addressing concerns of one sector with the opportunities of the other. Originality/value First, Education 4.0 and Industry 4.0 are reviewed in terms of opportunities and challenges they present. Second, a novel Twin Peaks model for the convergence of Education 4.0 and Industry 4.0 is presented. The proposed discovers that the convergence is adaptive, iterative and must be ethically sound while considering the broader societal implications of the digital transformation. Third, this study also acts as a torch-bearer for the necessity for more research of this kind to guarantee that our educational ecosystem is adaptable and capable of producing the skills required for success in the era of IR4.0.

Model-based System Engineering (MBSE) of the Internet of Things (IoT) literature is broad, and analysis of this literature enables the identification of themes and potential future study topics that will influence system development. This paper reports on bibliometric literature analysis of MBSE of IoT. It considers conference and journal publication trends in the state-of-the-art to identify emerging research themes from the standpoint of trans/multi-disciplinary scholarship and technology. We used Elsevier’s Scopus database to find relevant publications from January 2018 to December 2022. Using publication citation ranking and other factors (e.g., publication venues), we selected 110 articles and then analyzed them using BibExcel and VOSviewer software tools. With a modest decline in 2021, this analysis shows an overall increase in publications during the time period. A thematic analysis of the abstracts revealed a strong focus on the introduction of reference architectures and integration of MBSE with business and management methodologies like Agile and BPMN 2.0. Model-driven engineering and machine learning techniques are essential among the enablers for realization of complex heterogeneous IoT systems in the realm of Industry 4.0. We highlight these findings to better understand and meet the enduring challenge of scaling MBSE of IoT across diverse sectors like health, manufacturing, and transportation.

Reducing complexity in system architecture and design specifications, and more specifically from the software aspect, is essential. The architecture specifications focus on what the requirements and static aspects of systems are. The design specifications define dynamic aspects of computational components that sense and react to external stimuli. As the architecture and design specifications serve complementary roles in developing systems, the use of Architecture Analysis & Design Language (AADL) and Discrete Event System Specification (DEVS) is proposed for developing, in a step-wise fashion, combined architecture and design models. The proposed AADL-DEVS framework is grounded in the foundational modularity and hierarchy principles common to the AADL and DEVS modeling approaches. A realization of this framework capable of transforming and simulating the AADL-DEVS specifications is developed using the Open Source AADL Tool Environment (OSATE) and DEVS-Suite simulator. The scope of this paper is on the computational aspect of systems. The proposed AADL-DEVS framework is demonstrated using a model for the software part of an infant incubator, a time-sensitive and safety–critical system.

Assessment of multifaceted E-Learning literature lends itself to understanding and identifying themes and future research directions impacting STEM learning and teaching. This paper reports on bibliometric literature analysis of STEM E-Learning. It considers conference and journal publication trends in E-learning to identify emerging research themes from the standpoint of trans/multi-disciplinary scholarship and technology. We used Elsevier's SCOPUS database to find relevant publications from January 2013 to August 2022. Using publication citation ranking and other factors (e.g., publication venues), we selected 194 articles and then analyzed them using BibExcel and VOSviewer software tools. This study shows an increase in publications during the 2019-2020 period, followed by a decline beginning with the onset of the COVID-19 pandemic. A thematic analysis of the abstracts and selected full papers revealed a strong focus on utilizing mixtures of Augmented/Virtual Reality, simulations, and others for mixed-modality learning and teaching. Emerging technologies are essential for improving or creating new kinds of anywhere/anytime platforms needed for STEM virtual labs. We highlight these findings to understand better and meet the enduring challenge of scaling STEM E-Learning across diverse communities of students and educators at higher-education institutions.

PurposeSaudi universities have incorporated capstone projects in the final year of an undergraduate study. Although universities are following recommendations of the National Commission for National Commission for Academic Accreditation and Assessment (NCAAA) and Accreditation Board for Engineering and Technology (ABET), no detailed guidelines for management and assessment of capstone projects are provided by these accreditation bodies. Variation in the management and assessment practices of capstone project courses and analysis of the students' capabilities to align with industry demands, to realize Vision 2030, is challenging. This study investigates the current practices for structure definition, management and assessment criteria used for capstone project courses at undergraduate level for information technology (IT) programs at Saudi universities.Design/methodology/approachA web-based questionnaire is administered using a web service commonly used for questionnaires and polls to investigate the structure, management and assessment of capstone projects at the undergraduate level offering software engineering, computer science and information technology (SECSIT) programs. In total, 42 faculty members (with range of experience of managing/advising capstone projects from 1 to more than 10 years) from 22 Saudi universities (out of more than 30 universities offering SECSIT undergraduate programs) participated in the study.FindingsThe authors have identified that Saudi universities are facing challenges in the utilized process model, the distribution of work and marks, the knowledge sharing approach and the assessment scheme. To cope with these challenges, the authors recommend the use of an incremental development process, the utilization of a project-driven approach, the development of a national level digital archive and the implementation of homogeneous assessment scheme.Social implicationsTo contribute to the national growth and to fulfill the market demand, universities are recommended to align the capstone project courses with latest technology trends. Universities must collaborate with the industry and update the structure and requirements of capstone project courses accordingly. This will further facilitate to bridge the gap between industry and academia and will develop a win–win scenario for all the stakeholders.Originality/valueAlthough universities are committed to increase innovative capacities of their students for enabling them to contribute to economic and social growth, it is still hard to know the knowledge creation and sharing at national level. Variations in the management and assessment practices for capstone projects further intensify this challenge. Hence, there is a need of smart assessment and management of software capstone projects being developed in Saudi universities. Incorporating latest technologies, such unified management can facilitate discovering the trends and patterns related to the domain and complexity.

The dynamic and multi-dimensional quality assurance process for Saudi higher education institutes under the National Commission for Academic Accreditation and Assessment (NCAAA) demands an integrated framework for management and support of internal quality reviews and evidence-based self -studies in a cost-effective way. Due to cross-institutional involvement, quality assurance compliance with NCAAA standards is even more challenging for institutes offering courses with blended learning paradigm in multiple campuses. This papers proposes a Cloud-based framework to realize Quality Assurance and Enhancement as a Service (QAEaaS) to facilitate the internal quality reviews by providing efficient data management and effective communication for different stakeholders. Architecture of the proposed framework is described with respective features to cope with the identified quality assurance challenges and issues faced by the Saudi higher education institutes.

The Chinese Train Control System level 3 (CTCS-3) is an open and real-time safety-critical system. Due to the non-deterministic delay behavior in the environment, there is a large number of stimuli to the train control system with different patterns of arrival times. Control strategies must be well considered, as either the logic of the function fails or the real-time constraints are dissatisfied, may directly lead to significant human injury or financial loss. In this paper, we introduce the notion of test specification and the relativized timed input/output conformance based on timed automata theory. A new test case generation and execution algorithm has been proposed, by which the tester can reset Implementation Under Test (IUT) whenever they want, make it more sense in specific domain fields. We apply UPPAAL-TRON based online conformance testing framework to test nondeterministic delay behavior of Radio Block Center (RBC) handover scenario of CTCS-3 against critical safety, real-time, and liveness properties (defined in the system requirement specification (SRS) documents). Our experiments show that assurance of collision avoidance and train non-derailment can be guaranteed, but emergency brake intervention may happen with low probability in this scenario under the requirements specified in the SRS document.

Subjective well-being has a critical affect on progress and productivity vital for digital and strategical trans-formation. Increase in the suicide attempts of the college and university students is a clear indication of stress and anxiety among the students. Offering a fulfilling and healthy life to promote the life-long learning journey is also one of the important objectives of the Vision 2030 for modernization of the Kingdom of Saudi Arabia. Due to the multifaceted nature of subjective well-being, real-time mood measurement and reflection is a challenging task and demands using latest technologies. This paper aims to present Meezaj, an interactive system for real-time mood measurement and reflection leveraging the Internet of Things (IoT) technology. Architecture and workflow of the Meezaj system are discussed in detail. Meezaj not only promotes the sense of significance in the students, by indicating that their happiness matters in decision making, but also assists policy makers to identify factors affecting the happiness in an educational institute.

It is essential to use modeling methods for specifying real-time and safety-critical specifications and executions as a set of computational and physical components. Thus, frameworks supporting modular, hierarchical specifications at multiple levels of abstraction for software-intensive systems are needed. Models for the structures, behaviors, and relationships benefit from separating and combining external properties and internal operations of components. Together, the Architecture Analysis and Design Language (AADL) and Discrete-Event System Specification (DEVS) provide an integrated framework where the structure and behavior designs can be systematically developed and evaluated. Needs including latency and safety analyses are supported by AADL whereas behavioral verification and validation can be supported with DEVS simulation. To create the proposed AADL-DEVS framework, a DEVS behavioral annex targeted for the DEVS-Suite simulator is developed and introduced to OSATE which supports AADL. The DEVS Annex language is detailed and exemplified using an infant incubator known as the Isolette system.

AADL is a Model-Based Engineering language for architectural analysis and specification of real-time embedded systems with stringent performance requirements (e.g. fault-tolerance, security, safety-critical etc.). However, core AADL lacks of a mechanism for modeling continuous evolution of physical processes which are controlled by digital controllers. In our previous work, we have introduced Hybrid Annex—an AADL extension for continuous behavior and cyber-physical interaction modeling based on Hybrid Communicating Sequential Processes (HCSP). In this paper, we present formal semantics of the synchronous subset of AADL models annotated with Hybrid Annex specifications using HCSP. The semantics are then used to verify correctness of AADL models (with Hybrid Annex specifications) using an in-house developed theorem prover — Hybrid Hoare Logic (HHL) prover.

Train control systems like most digital controllers are, by definition, hybrid systems as they interact with or try to control some aspects of the physical world. Detailed behavior modeling with constraints specification and formal verification, required for reliability prediction, is a great challenge for hybrid system designers. Train control systems further intensify this challenge with extensive interaction between computing units and their physical environment and their mutual dependence on each other. In this paper, we investigate behavior modeling and formal verification of Chinese Train Control System Level 3 (CTCS-3) using Architectural Analysis & Design Language (AADL) to cope with this challenge. AADL is an architecture description language for embedded systems and is based on model-based engineering paradigm. Along with structural modeling of embedded systems using the core language constructs, AADL also provides support for language extension through annex sublanguages. In system requirements specification document, the behavior of the CTCS-3 is specified as a set of basic operation scenarios that cooperate with each other to achieve safe and secure functionality of trains. Movement Authority (MA) scenario, explored in this paper, is considered as a basic and most crucial scenario to prevent trains from colliding with each other. The detailed discrete behavior of control system is modeled and verified using the Behavior Language for Embedded Systems with Software (BLESS) annex sublanguage of AADL, and the continuous behavior of train with the cyber–physical interaction (communication between train and control system) is modeled using the Hybrid annex sublanguage. The behavior of the MA scenario at system level is verified using the Hybrid Hoare Logic theorem prover. Behavior constraints are specified as assertions using first-order logic formulas augmented with a simple temporal operator.

Correct design, and system-level dependability prediction of highly-integrated systems demand the collocation of requirements and architectural artifacts within an integrated development environment. Hybrid systems, having dependencies and extensive interactions between their control portion and their environment, further intensify this need. AADL is a model-based engineering language for the architectural design and analysis of embedded control systems. Core AADL has been extended with a mechanism for discrete behavioral modeling and analysis of control systems, but not for the continuous behavior of the physical environment. In this paper, we introduce a lightweight language extension to AADL called the Hybrid Annex for continuous-time modeling, fulfilling the need for integrated modeling of the computing system along with its physical environment in their respective domains. The Isolette system described in the FAA Requirement Engineering Management Handbook is used to illustrate continuous behavior modeling with the proposed Hybrid Annex.