This paper presents the Smart Local Search (SLS) algorithm, a hybrid metaheuristic framework for the NP-hard examination timetabling problem. SLS distinctively integrates graph-based construction heuristics with a guided local search framework, enhanced by an aspiration criterion to recover promising solutions overlooked by penalty terms and a strategic random move mechanism to escape local optima. Extensive experiments on all 11 of Carter’s widely used benchmark datasets show that SLS achieves competitive results, with an average penalty of 28.03 and a standard deviation of 42.30 across the benchmarks. Statistical significance testing (Wilcoxon signed-rank test, α = 0.05) confirms that SLS’s performance is significantly better than most baseline methods (p-value−10). The algorithm demonstrates particular strength in stability and consistency, making it a robust and efficient solution for complex educational scheduling environments.

This work focuses on Real-time system models based on the Time Petri Net (TPN) formalism and addresses a pathological aspect known to often affect models of Real-Time Systems called Zeno Behavior or Zenoness. Zenoness permits a system’s model to perform an unbounded number of actions in a finite amount of time, which violates a fundamental requirement for real-time systems that they can’t be infinitely fast. To verify Zenoness on TPNs, the only known technique requires translating a TPN into an equivalent timed automaton, then performing the test on the translation, losing in the process performance and the ease of interpreting the results back and forth between the original model and its translation. In this work, we propose an efficient approach to model-check Zenoness directly on the TPN model. We start by stating a necessary and sufficient condition for TPNs to be Zeno, then derive some interesting structural properties regarding Zenoness and an efficient algorithm to model-check Zenoness for bounded TPNs. Our results provide a good insight into how to avoid Zenoness during design time, how to spot the problem when it occurs, and how to rectify it.Note to Practitioners—When designing a Real-time system for critical industrial applications, we are often required to model the system using some mathematical formalism. The objective is to formally verify that our design meets some important functional and non-functional requirements when it is implemented. Mathematical formalisms such as Timed Automata (TA) and timed extensions of Petri Nets are often used for that purpose. One of these extensions called Time Petri Net (TPN) is known to be intuitive and simple, yet very versatile and powerful. When creating a model for a Real-time system, one critical aspect called Zenoness is often neglected or unforeseen. Zenoness is a modeling flaw that can easily be unintentionally injected during the modeling phase of a Real-time system but is often very difficult to spot. A model is Zeno if it can perform infinitely many actions in a finite amount of time. Although this behavior is unrealistic for Real-time systems, it can lead to false conclusions during the verification process of the model and catastrophic implications for the implemented system. An approach has been developed to verify Zenoness for the TA formalism, but no method exists yet to verify Zenoness directly on TPNs. In this work, we show how to efficiently verify Zenoness directly on the TPN formalism, and provide some useful insights into how to minimize the risk of unintentionally injecting Zenoness in a TPN model during design time.

International audience

According to the IEC 62351-7 standard, data collection using network and system management (NSM) can be used to support the security monitoring of the smart grid. In this article, an NSM security monitoring platform for a realistic IEC 61850 substation model is developed using the specifications provided in IEC 62351-7. In the developed model, grid measurements are ready to take operative decisions, whereas collected NSM data are leveraged to detect cyberattacks and/or identify anomalies. The model includes power components (e.g., transformers, lines, and generators), controllers (e.g., voltage control), protection devices (e.g., overcurrent, distance, differential, and under/overvoltage), communication protocols (e.g., sampled value and generic object-oriented substation event), and NSM (e.g., agents and managers) applications. Moreover, a two-step deep learning framework is proposed for anomaly detection and cyberattack identification with enhanced accuracy. The first step can apply long short-term memory, recurrent neural network, and gated recurrent units, each in combination with an autoencoder. Then, the ensemble learning technique is used in the second step to augment the outputs of these deep learning models. To evaluate the effectiveness of the proposed cyberattack and anomaly detection framework, we detail and simulate potential cyberattacks targeting the performance of the IEEE 9-bus system. The proposed anomaly detection scheme can identify these threats using NSM data in a hardware-in-the-loop testbed. Finally, based on our assessment results, recommendations are provided for cybersecurity guidelines concerning IEC 62351-7.

The precision time protocol (PTP) is considered as one of the most favorable mechanisms for providing unified and precise time at the substation level in the smart grid. Nevertheless, PTP was shown to be vulnerable to cyber-attacks targeting its components and synchronization services. In this article, we capitalize on the theory and outcome of our previous work to contribute a more complete solution that addresses PTP cyber security. We propose to close the PTP loop through an extension that introduces new functionality and messages. This extension covers the PTP attack surface and enables the detection of attacks on PTP time synchronization. We formally model and verify the proposed extension using UPPAAL model checker. In addition, we validate the proposed extension using Omnet++ simulation. The evaluation demonstrates that our approach preserves PTP functionality, while successfully detecting cyber attacks against PTP components in a timely manner.

The growth of cloud-based services is mainly supported by the core networking infrastructures of large-scale data centers, while the scalability of these services is influenced by the performance and dependability characteristics of data centers. Hence, the data center network must be agile and reconfigurable in order to respond quickly to the ever-changing application demands and service requirements. The network must also be able to interconnect the big number of nodes, and provide an efficient and fault-tolerant routing service to upper-layer applications. In response to these challenges, the research community began exploring novel interconnect topologies, namely: Flecube, DCell, Ficonn, HyperFlaNet and BCube. However, these topologies either scale too fast (grows exponentially in size), or too slow, and therefore suffer from performance bottlenecks. In this paper, we propose a novel data center topology called LaScaDa (Layered Scalable Data Center) as a new solution for building scalable and cost-effective data center networking infrastructures. The proposed topology organizes nodes in clusters of similar structure, then interconnect these clusters in a well-crafted pattern and system of coordinates for nodes to reduce the number of redundant connections between clusters, while maximizing connectivity. LaScaDa forwards packets between nodes using a new hierarchical row-based routing algorithm. The algorithm constructs the route to the source based on the modular difference between the source and destination coordinates. Furthermore, the proposed topology interconnects a large number of nodes using a small node degree. This strategy increases the number of directly connected clusters and avoids redundant connections. As a result, we get a good quality of nodes in terms of average path length (APL), bisection bandwidth, and aggregated bottleneck throughput. Experimental results show that LaScaDa has better performance than DCell, BCube, and HyperBcube in terms of scalability, while providing a good quality of service.

Many proposed data center architectures are constructed with a huge number of network devices in order to support the increasing cloud based services. These devices are used to achieve the highest performance in case of full utilization of the network. However, the peak capacity of the network is rarely reached. As a result, many devices are set into idle state which increases the network energy consumption and lead to a non-proportionality between the consumed energy and the network load. In this paper, we present a new approach that reduces the data center energy consumption with a reduced trade off on network performance. By exploiting the correlation in time of internode communication and some topological features, the proposed approach uses the outdated traffic matrix to control the set of active communication links and ports in the network (switches ports and nodes ports). The ports activation management process is done using a proposed algorithm that guarantees network connectivity. Extensive simulations have been conducted to validate the performance of the proposed scheme in terms of average path length and energy consumption.

The study of biological systems is growing rapidly, and can be considered as an intrinsic task in biological research, and a prerequisite for diagnosing diseases and drug development. The integration of biological studies with computer technologies led to noticeable developments in biology with the appearance of many powerful modeling and simulation techniques and tools. The help of computers in biology resulted in deeper knowledge about complex biological systems and biopathways behaviors. Among modeling tools, the Petri Net formalism plays an important role. Petri Net is a powerful computerized and graphical modeling technique originally developed by Carl Adam Petri in 1960 to model discrete event systems. With its various extensions, Petri Nets find applications in many other fields including Biology. The extension known under the name Hybrid Functional Petri Net (HFPN) was developed specifically to model biological systems. Traditionally, biological processes are captured as systems of ordinary differential equations (ODEs). However, HFPNs offer a much more elegant and versatile approach to represent these processes more accurately. In fact, HFPNs allow to capture phenomena which are impossible to capture with ODES, while being more intuitive and easy to understand and model with. In this work we propose an approach to translate a system of ODEs representing a biological process into a HFPN. The resulting HFPN, not only preserves the semantics of the original model, but is also more humanly readable thanks to the use of a novel technique to connect its components in a smart way. To validate our approach, we implemented it as an extension to the tool Real Time Studio (an integrated environment for modeling, simulation and automatic verification of real-time systems), and compared our simulation results with those obtained by simulating systems of ODEs using MATLAB.

We propose a new framework for social-sensor cloud services selection based on spatio-textual correlation between user's query and service. The proposed research defines a formal social-sensor cloud service model that abstracts the functional and non-functional aspects of social-sensor data on the cloud in terms of spatio-temporal, textual and quality of service parameters. Proposed framework is a 4-stage filtering algorithm, to select social-sensor cloud services based on user query and quality of service demands. 4-stage filtering is based on spatial correlation, textual correlation, visual features and quality of service parameters. Analytical results are presented to show the performance of the proposed approach.

We propose a 'Sentiment Analysis as a Service' (SAaaS) framework that abstracts sentiments from social information services, analyses and transforms into useful information. We propose a dynamic service composition mechanism for sentiment analysis based on the social information service classification. We also propose a new quality model to assess the quality of social information services. We use social media based public health surveillance as a motivating scenario. In particular, we focus on the spatio-temporal properties of social media users' sentiments to identify the locations of disease outbreaks. Experiments are conducted on the real-world datasets. Analytical results preliminarily show the performance of our proposed approach.

We propose in this paper some efficient approaches, based on the state class graph method, to construct abstractions for the Time Petri Net (TPN) model, suitable to verify its linear or reachability properties. Experimental results have shown that these abstractions are very appropriate as both time and size are considerably reduced. For some tested models, abstractions that preserve reachability properties can be as many as 2,051 times smaller and more than 592 times faster to compute. For abstractions, which are overapproximations (useful to prove that certain states are not reachable), gains can overpass 10,000 for both time and size.

In this paper we develop a security verification framework for open source software with a multi-language support. We base our approach on the GCC compiler which is considered as the defacto open source compiler for several languages including C, C++, JAVA, ADA, FORTRAN,etc. To achieve our goal we use a conventional push down system model-checker for reachability properties, and turn it into a fully-fledged verification tool for both low and high level software security properties. We also allow programmers to define a wide range of temporal security properties using an automata-based specification approach. As a result, our approach can model-check large scale software against system-specific security properties.