Artificial Intelligence (AI) and data are reshaping organizations and businesses. Human Resources (HR) management and talent development make no exception, as they tend to involve more automation and growing quantities of data. Because this brings implications on workforce, career transparency, and equal opportunities, overseeing what fuels AI and analytical models, their quality standards, integrity, and correctness becomes an imperative for those aspiring to such systems. Based on an ontology transformation to B-machines, this article presents an approach to constructing a valid and error-free career agent with Deep Reinforcement Learning (DRL). In short, the agent's policy is built on a framework we called Multi State-Actor (MuStAc) using a decentralized training approach. Its purpose is to predict both relevant and valid career steps to employees, based on their profiles and company pathways (observations). Observations can comprise various data elements such as the current occupation, past experiences, performance, skills, qualifications, and so on. The policy takes in all these observations and outputs the next recommended career step, in an environment set as the combination of an HR ontology and an Event-B model, which generates action spaces with respect to formal properties. The Event-B model and formal properties are derived using OWL to B transformation.

Until now, only the PID has been used to control DC/DC converters for a Nanosatellite’s Electrical Power System (EPS), thus, the goal of this work is to investigate the feasibility of other methods. This paper focuses on a comparative study of SMC and LQR for the regulation of a Buck converter used in EPS. A study is done to evaluate their efficiency, using MATLAB/Simulink, in response to various fluctuations in voltage source, reference voltage and resistive load. To estimate the system’s states and filter the noise in the measurements, a Kalman filter is utilized. In terms of recovery time, settling time and under/overshoots, SMC outperforms the other controllers, however, the control input suffers from the chattering effect and high magnitude peaks. The SMC recovery time to a change in the load is 0.677ms, while LQR takes 1.583ms to recover. PID, on the other hand, is slower with a recovery time of 3.068ms. SMC also presents the lowest steady state error which is less than 0.01%, whereas LQR and PID have an error less than 0.36% and 0.56%, respectively.

Formalizing system specification has been highly valuable in demonstrating safety and consistence of safety critical systems. It is undoubtedly the case in railway signalling, especially the European Rail Traffic Management System/European Train Control System (ERTMS/ETCS). However, the complexity of the European standard specification, especially for its highest level, namely level 3, requires a significant overtake in early modelling approaches when it comes to clearly expressing system functionalities along with safety requirements, all towards a concrete safe design. In this regard, our research introduces a Colored Petri net (CPN) sub-class associated to an Event-B machine and annotated by mathematical sequences, which are ex-pressed in the B-language, all in the view of enriching the modelling techniques intended for system formal specification and verification. In this paper, we show through a detailed ERTMS L3 case study, how such featured CPNs fit in the progressive formalization and verification of Movement Authority (MA) computation.