The use of DNS over HTTPS (DoH) tunneling by an attacker to hide malicious activity within encrypted DNS traffic poses a serious threat to network security, as it allows malicious actors to bypass traditional monitoring and intrusion detection systems while evading detection by conventional traffic analysis techniques. Machine Learning (ML) techniques can be used to detect DoH tunnels; however, their effectiveness relies on large datasets containing both benign and malicious traffic. Sharing such datasets across entities is challenging due to privacy concerns. In this work, we propose CO-DEFEND (Continuous Decentralized Federated Learning for Secure DoH-Based Threat Detection), a Decentralized Federated Learning (DFL) framework that enables multiple entities to collaboratively train a classification machine learning model for DoH threat detection while preserving data privacy, enhancing scalability and resilience against single points of failure. The proposed DFL framework provides a realistic implementation for DoH threat detection, enabling multiple entities to train their local models online with incoming DoH flows in real-time batches as they are processed – an approach that fits naturally within modern Internet architectures. This framework adapts four classical machine learning algorithms, Support Vector Machines (SVM), Logistic Regression (LR), Decision Trees (DT), and Random Forest (RF), for federated scenarios and efficient training. In addition, a key methodological feature of CO-DEFEND is the use of DT and RF as model selection rather than aggregation mechanisms, allowing each participant to retain interpretable and locally optimal decision structures while benefiting from collective updates. We compare our proposed method by using the dataset CIRA-CIC-DoHBrw-2020 with existing machine learning approaches, including more computationally complex alternatives such as neural networks, to demonstrate its effectiveness in detecting malicious DoH tunnels while improving scalability and computational efficiency.

Distributed AI and IoT applications increasingly execute across heterogeneous resources spanning end devices, edge/fog infrastructure, and cloud platforms, often under different administrative domains. Fluid Computing has emerged as a promising paradigm for enhancing massive resource management across the computing continuum by treating such resources as a unified fabric, enabling optimal service-agnostic deployments driven by application requirements. However, existing solutions remain largely centralized and often do not explicitly address multi-domain considerations. This paper proposes an agnostic multi-domain orchestration architecture for fluid computing environments. The orchestration plane enables decentralized coordination among domains that maintain local autonomy while jointly realizing intent-based deployment requests from tenants, ensuring end-to-end placement and execution. To this end, the architecture elevates domain-side control services as first-class capabilities to support application-level enhancement at runtime. As a representative proof of concept, we instantiate the architecture through a distributed AI use case; specifically, we consider a multi-domain Decentralized Federated Learning (DFL) deployment under Byzantine threats. Under this setting, we leverage domain-side capabilities to enhance Byzantine security by introducing FU-HST, an SDN-enabled multi-domain anomaly detection mechanism that complements Byzantine-robust aggregation. We validate the use-case workflow via simulation in single- and multi-domain settings, evaluating anomaly detection, DFL performance, and computation/communication overhead.

Quantum Key Distribution (QKD) promises information-theoretic security, yet integrating QKD into existing protocols like TLS remains challenging due to its fundamentally different operational model. In this paper, we propose a hybrid QKD-KEM protocol with two distinct integration approaches: a client-initiated flow compatible with both ETSI 004 and 014 specifications, and a server-initiated flow similar to existing work but limited to stateless ETSI 014 APIs. Unlike previous implementations, our work specifically addresses the integration of stateful QKD key exchange protocols (ETSI 004) which is essential for production QKD networks but has remained largely unexplored. By adapting OpenSSL’s provider infrastructure to accommodate QKD’s pre-distributed key model, we maintain compatibility with current TLS implementations while offering dual layers of security. Performance evaluations demonstrate the feasibility of our hybrid scheme with acceptable overhead, showing that robust security against quantum threats is achievable while addressing the unique requirements of different QKD API specifications.

Fluid Computing has emerged as a promising paradigm for enhancing massive and heterogeneous resource management across the Cloud-to-Edge continuum for Internet of Things (IoT) and artificial intelligence (AI) applications. Despite its advantages, research into the optimal deployment of distributed applications across fluid scenarios remains scarce, and existing centralized frameworks cannot exploit emerging AI-native features nor model realistic multi-domain deployment scenarios. This paper presents an innovative provider-based architecture for the optimal orchestration of distributed AI services in fluid environments under 6G network capabilities. The proposed hybrid solution includes robust and scalable decentralized orchestration for the placement of cross-provider workloads without a central broker, as well as leveraging autonomous decision-making devices through distributed task offloading techniques. The proposal was tailored to a Decentralized Federated Learning deployment, serving as a use case in settings with strict privacy and security requirements. This approach was adopted to illustrate the viability of the proposal by deploying large distributed AI services in 6G-like networks.

The rapid growth of Internet of Things (IoT) devices and applications has led to an increased demand for advanced analytics and machine learning techniques capable of handling the challenges associated with data privacy, security, and scalability. Federated learning (FL) and blockchain technologies have emerged as promising approaches to address these challenges by enabling decentralized, secure, and privacy-preserving model training on distributed data sources. In this paper, we present a novel IoT solution that combines the incremental learning vector quantization algorithm (XuILVQ) with Ethereum blockchain technology to facilitate secure and efficient data sharing, model training, and prototype storage in a distributed environment. Our proposed architecture addresses the shortcomings of existing blockchain-based FL solutions by reducing computational and communication overheads while maintaining data privacy and security. We assess the performance of our system through a series of experiments, showing its potential to enhance the accuracy and efficiency of machine learning tasks in IoT settings.

Continual learning (CL) poses the important challenge of adapting to evolving data distributions without forgetting previously acquired knowledge while consolidating new knowledge. In this paper, we introduce a new methodology, coined the Tabular-data Rehearsal-based Incremental Lifelong Learning framework (TRIL3), designed to address the phenomenon of catastrophic forgetting in an online, task-free setting. TRIL3 utilizes an Incremental Learning Vector Quantization (ILVQ) algorithm as an efficient prototype-based incremental generative model to store and generate synthetic data to preserve knowledge over time, and the Deep Neural Decision Forest (DNDF) algorithm, which was modified to run incrementally to learn supervised classification tasks for tabular data. Based on tests conducted to determine the optimal percentage of synthetic data and comparisons with other available task-free CL proposals, we conclude that TRIL3 outperforms other methods in the literature using only 50% of synthetic data.

Federated Learning (FL) is a machine learning framework that enhances privacy compared to normal FL, since model training is done across multiple nodes by exchanging only local parameters instead of raw data. Despite this advantage, FL is still vulnerable to some privacy attacks that have been addressed with techniques such as Differential Privacy (DP), Homomorphic Encryption (HE), or Secure Multi-Party Computation (SMPC). These methods need further assumptions that narrow their range of application, exhibiting problems to work with non-linear functions, to perform large matrix multiplications and having high communication and computational costs to manage semi-honest nodes. In this paper, we propose a solution to guarantee privacy in FL schemes that simultaneously solves these shortcomings. Our proposal is based on the Berrut Approximated Coded Computing (BACC), a technique from the coded computing paradigm, adapted here to provide input privacy to FL in a scalable way. In our Private BACC, controlled randomness is introduced into the rational Berrut approximation of a target function so that the input values are hidden and the output function values can still be computed with good approximation. We provide a theoretical bound to the privacy leakage level of private BACC, and further describe its application for computing arbitrary non-linear functions, particularly distributed matrix multiplications. Our numerical results demonstrate that adding privacy in this form outperforms DP in model quality, since it has negligible cost in the precision. Additionally, it beats HE in terms of computational cost, and requires lower computation and communications costs than with SMPC algorithms. Finally, the proposed method supports distributed matrix multiplications, so it can be integrated into a wide class of machine learning systems.

Decentralised machine learning has recently been proposed as a potential solution to the security issues of the canonical federated learning approach. In this paper, we propose a decentralised and collaborative machine learning framework specially oriented to resource-constrained devices, usual in IoT deployments. With this aim we propose the following construction blocks. First, an incremental learning algorithm based on prototypes that was specifically implemented to work in low-performance computing elements. Second, two random-based protocols to exchange the local models among the computing elements in the network. Finally, two algorithmics approaches for prediction and prototype creation. This proposal was compared to a typical centralized incremental learning approach in terms of accuracy, training time and robustness with very promising results.

Abstract Lifelong learning requires appropriate solutions, especially for corporate training. Workers usually have difficulty combining training and their normal work. In this context, micro-learning emerges as a suitable solution, since it is based on breaking down new concepts into small fragments or pills of content, which can be consumed in short periods of time. The purpose of this paper is twofold. First, we offer an updated overview of the research on this training paradigm, as well as the different technologies leading to potential commercial solutions. Second, we introduce a proposal to add micro-learning content to more formal distance learning environments (traditional Learning Management Systems or LMS), with the aim of taking advantage of both learning philosophies. Our approach is based on a Service-Oriented Architecture (SOA) that is deployed in the cloud. In order to ensure the full integration of the micro-learning approach in traditional LMSs, we have used two well-known standards in the distance learning field: LTI (Learning Tools Interoperability) and LIS (Learning Information Service). The combination of these two technologies allows the exchange of data with the LMS to monitor the student’s activity and results. Finally, we have collected the opinion of lectures from different countries in order to know their thoughts about the potential of this new approach in higher education, obtaining positive feedback.

Undoubtedly, Location-based Social Networks (LBSNs) provide an interesting source of geo-located data that we have previously used to obtain patterns of the dynamics of crowds throughout urban areas. According to our previous results, activity in LBSNs reflects the real activity in the city. Therefore, unexpected behaviors in the social media activity are a trustful evidence of unexpected changes of the activity in the city. In this paper we introduce a hybrid solution to early detect these changes based on applying a combination of two approaches, the use of entropy analysis and clustering techniques, on the data gathered from LBSNs. In particular, we have performed our experiments over a data set collected from Instagram for seven months in New York City, obtaining promising results.

Smart Grid is considered entirely indispensable in the next generation of electricity networks since shifting from the conventional to the cyber-physical power grids; relying on the Advanced Metering Infrastructures (AMIs) where a bidirectional communication with the utility provider supports improved reliability and satisfaction of customers' needs. Moreover, Smart Grid promises self-healing, i.e., automatic and quick detection and analysis of faults and failures. Unfortunately, the new grid turns into an information system and as such, it becomes vulnerable to cyber-risks and cyber-threats so that specific cyber-attacks can be directed to either Smart Grids or Microgrids (small-scale form of grids that contain distributed generators and power-storage units). In this new scenario, it is highly required to be cyber-resilient and to detect anomalies in the Smart Grid such as misusage, system faults or cyber-security incidents. Although anomalies could be detected in a holistic approach over a Cloud Computing infrastructure, this research paper proposes Fog Computing model to detect the anomalous patterns in the electricity consumption data by means of collaboration of distributed devices at the edge of Smart Grid network enough in advance (reducing communication latencies). The implementation of the proposed solution follows the Open-Fog Reference Architecture (RA) and a Microgrid on premises of the university of Vigo for a preliminary result as a proof of concept.

Abstract Over the last decade, the infrastructure supporting the smart city has lived together with and was surpassed by the rise of social media. The tremendous growth of both mobile devices and social media users has unearthed a new kind of services in the so‐called location‐based social networks (LBSNs). In this new scenario, the term crowdsensing refers to sharing data collected by sensing humans with the aim of measuring phenomena of common interest. Crowd‐sourced location data provide the ability to study, for the first time, the movement of individuals in urban environments. In this paper, we address the problem of monitoring crowds, whereabouts and movement, which can assist decision making in education, emergency training, urban planning, traffic engineering, etc. Precisely, two‐phase density‐based analysis for collectives and crowds (2PD‐CC) is a novel methodology over public data in LBSN, which combines density‐based clustering, outlier detection a topic modeling over a region under study to detect, predict, and explain abnormal group behavior. In order to validate the methodology and its potential application to full‐scale problems, an experiment over Twitter data was performed in Madrid city.

There is a general consensus of the good sensing and novelty characteristics of Twitter as an information media for the complex financial market. This paper investigates the permeability of Twittersphere, the total universe of Twitter users and their habits, towards relevant events in the financial market. Analysis shows that a general purpose social media is permeable to financial-specific events and establishes Twitter as a relevant feeder for taking decisions regarding the financial market and event fraudulent activities in that market. However, the provenance of contributions, their different levels of credibility and quality and even the purpose or intention behind them should to be considered and carefully contemplated if Twitter is used as a single source for decision taking. With the overall aim of this research, to deploy an architecture for real-time monitoring of irregularities in the financial market, this paper conducts a series of experiments on the level of permeability and the permeable features of Twitter in the event of one of these irregularities. To be precise, Twitter data is collected concerning an event comprising of a specific financial action on the 27th January 2017: the announcement about the merge of two companies Tesco PLC and Booker Group PLC, listed in the main market of the London Stock Exchange (LSE), to create the UK’s Leading Food Business. The experiment attempts to answer two research questions which aim to characterize the features of Twitter permeability to the financial market. The experimental results confirm that a far-impacting financial event, such as the merger considered, caused apparent disturbances in all the features considered, that is, information volume, content and sentiment as well as geographical provenance. Analysis shows that although Twitter is not a specific financial forum, it is permeable to financial events. Therefore it should be considered within the architecture for real-time monitoring of irregularities in the financial market.

iBeacon advertising technology transmits relevant, targeted messages and information to smart devices by using Bluetooth Low Energy (BLE) protocol. These devices, as far as the literature shows, are configured to send the same information to all devices (static). In this work, we propose a customized dynamic iBeacon content distribution system with the implementation challenges and what it takes to develop the solution. In such system, single beacon device recognizes multiple users and put them into different profiles. For that process, the system uses a user's device MAC address and his entrance timestamp when he enters the beacon advertising area. After that, a corresponding content (dynamically selected) is automatically sent to the recognized profiles.

Citizens are actively interacting with their surroundings, especially through social media. Not only do shared posts give important information about what is happening (from the users’ perspective), but also the metadata linked to these posts offer relevant data, such as the GPS-location in Location-based Social Networks (LBSNs). In this paper we introduce a global analysis of the geo-tagged posts in social media which supports (i) the detection of unexpected behavior in the city and (ii) the analysis of the posts to infer what is happening. The former is obtained by applying density-based clustering techniques , whereas the latter is consequence of applying content aggregation techniques. We have applied our methodology to a dataset obtained from Instagram activity in New York City for seven months obtaining promising results. The developed algorithms require very low resources, being able to analyze millions of data-points in commodity hardware in less than one hour without applying complex parallelization techniques. Furthermore, the solution can be easily adapted to other geo-tagged data sources without extra effort.

Internet of Things (IoT) merges different technologies to provide the needed infrastructure for an adequate inter‐device connection and data exchange, with Bluetooth Low Energy (BLE) being one of the latest acquisitions. The use of BLE beacons offers a straightforward approach to broadcast information to any device being in the coverage zone and able to process such signal. Instead of this static solution, in this paper, we face an alternative approach that, combining both Wi‐Fi and BLE beacon technologies, is able to dynamically adapt the information being broadcast depending on the particular devices in the coverage area. Taking advantage of the beacon device communications, we propose to monitor the space occupancy throughout the study area (typically inside a building) by following the beacon device data exchange. This information would be later used to improve space analysis. As a proof of concept, we have conducted an experiment inside a faculty to check the potentiality of the proposal, obtaining promising results.

Although there are several tools available to simulate a Wireless sensor networks (WSN), few of them allow on-line simulation as WebShawn does. The tool can be considered as a complement of the existing experimental platforms allowing focus on implementation, collection, and analysis of data, in a relatively simple manner. The adopted software architecture is based on the remote simulation and visualization model, where the simulation engine is located at the server side, and the access to the simulation system is performed using a conventional web browser, obtaining the results through the Internet interface. This particular option is the main advantage of WebShawn regarding other existing applications. Being tested in the classroom as well as in a laboratory research, WebShawn is a tool ready for use by Information and Communications Technology (ICT) industry, researchers, students, or whoever needs to simulate WSN scenarios with a huge number of nodes. WebShawn allows users to assign their efforts to develop, design the network, and plan the scene, without losing time in the installation stage.

The great acceptation of the Social Web has converted social networks, blogs and wikis in almost perfect advertising mediums. However, many of the current social publicity strategies do not exploit all the potential of these mediums, since they obviate users' online life: the social contexts in which they are involved. Our proposal to reverse this situation is a model to infer users' social contexts by the application of several Natural Language Processing (NLP) and data mining techniques over users' interaction data on Facebook. We take advantage of both Facebook and Groupon APIs to provide a deployment scenario in which knowing users' social life allows ads to target the most potential customers, which is beneficial for both companies and possible customers.

In the new technological context of interactive digital (IDTV), traditional TV spots are expected to be replaced by interactive applications. In this paper, we propose a new TV advertising architecture inspired by the philosophy and business models of online advertising. Personalization and content awareness are the two mainstays of our approach that allow advertisers to have more efficient campaigns focused on a targeted audience.

One of the main ideas of agile development is to perform continuous integration, in order to detect and resolve conflicts among several modular units of a system as soon as possible. Whereas this feature is well catered for at the level of programming source code, the support available in formal specification environments is still rather unsatisfactory: it is possible to analyze the composition of several modular units automatically, but no assistance is given to help modify them in case of problems. Instead, the stakeholders who build the specifications are forced to attempt manual changes until reaching the desired functionality, in a process that is far from being intuitive. In response to that, this paper presents procedures and algorithms that automate the whole process of doing integration analyses and generating revisions to solve the diagnosed problems. These mechanisms serve to complete an agile specification environment presented in a previous paper, which was designed around the principle of facilitating the creative efforts of the stakeholders.

One of the main needs when dealing with multi-perspective specifications is to be able to have at our disposal, at intermediate stages of the development process, a merged view which properly reflects the knowledge of each participant in the elicitation tasks (and over which we can reason, even in the presence of disagreement and incompleteness). We show in this paper to what extent there can be many merged models, having all of them useful application. So there is not a unique operator which can be qualified as the best; on the contrary, there will be a suitable merging operator depending on the goal of the merging process. More concretely, we will propose a set of four composition operators: ∐max, ∐min, ∐majand ∐maj + inc. They will be evaluated making use of a list of desired algebraic properties proposed by researchers on merging and which should be held by an ideal merging operator. This analysis can help us to compare the different operators, revealing the key features of each, and identifying weaknesses that may require further research. The conclusion drawn after this analysis points out that these properties are not useful enough to adequately characterize a merging operator. Therefore, new properties will be provided in order to complete the previous list and help to define better the behavior of the different merging operators.

Abstract Digital Television will bring a significant increase in the amount of channels and programs available to end users, with many more difficulties to find contents appealing to them among a myriad of irrelevant information. Thus, automatic content recommenders should receive special attention in the following years to improve their assistance to users. The current content recommenders have important deficiencies that hamper their wide acceptance. In this paper, we present a new approach for automatic content recommendation that significantly reduces those deficiencies. This approach, based on Semantic Web technologies, has been implemented in the AdVAnced Telematic search of Audiovisual contents by semantic Reasoning tool, a hybrid content recommender that makes extensive use of well‐known standards, such as Multimedia Home Platform, TV‐Anytime and OWL. Also, we have carried out an experimental evaluation, the results of which show that our proposal performs better than other existing approaches. Copyright © 2007 John Wiley & Sons, Ltd.

This paper presents a practical approach to manage mobile ad-hoc networks around the service requirements of their forming hosts. The solution consists of a middleware layer called KEPPAN, designed to exploit incomplete and changeable information about virtually any aspect that influences service provision. Having formal languages at the interfaces with the networking and application levels, this approach represents a step towards autonomic, self-managed networks of mobile devices, in expectation of further advances in software engineering and artificial intelligence. Preliminary evaluation results are reported.

The generalized arrival of Digital TV will lead to a significant increase in the amount of channels and programs available to end users, making it difficult to find interesting programs among a myriad of irrelevant contents. Thus, in this field, automatic content recommenders should receive special attention in the following years to improve assistance to users. Current approaches of content recommenders have significant well-known deficiencies that hamper their wide acceptance. In this paper, a new approach for automatic content recommendation is presented that considerably reduces those deficiencies. This approach, based on the so-called Semantic Web technologies, has been implemented in the AVATAR tool, a hybrid content recommender that makes extensive use of well-known standards, such as TV-Anytime and OWL. Our proposal has been evaluated experimentally with real users, showing significant increases in the recommendation accuracy with respect to other existing approaches.

Content personalization is a very important aspect in the field of e-learning, although current standards do not fully support it. In this paper, we outline an extension to the ADL SCORM (Sharable Content Object Reference Model) standard in an effort to permit a suitable adaptivity based on user's characteristics. Applying this extension, we can create adaptable courses, which should be personalized before shown to the student.

Software development can be seen as a process of knowledge acquisition, in which human beings progressively learn about the intended behavior of the desired systems. Thereby, development is subject to considerable amounts of uncertainty and variability, that make it impossible to proceed in a purely incremental fashion — at some points, the need always arises to reconsider part of the accumulated knowledge. With this problem in mind, agile development methodologies have been gaining popularity in recent years as a means to enhance productivity, and there have been attempts to supplement them with formal techniques for better reliability. However, the existing approaches to agile formal methods have practically limited themselves to adopting recommended practices of agile development, with no particular contribution from the employed formalisms. Compared to that, this paper advocates the use of formalisms intended for evolutionary development, with a two-fold objective: first, to exploit the knowledge acquired up to any given stage as a means to cope with frequent and numerous changes; and, second, to introduce support for the creative development tasks through an interactive procedure that helps taking steps forward.

The development of requirements specifications is characterized by the uncertain and changeable knowledge available about the systems to be built. This paper presents a many-valued logic that enables effective reasoning about uncertainty and inconsistency in requirements specifications, motivating the election of six truth values and the definition of a new implication connective. The adequacy of this logic to support a formal development methodology is assessed through a comparison with Belnap's four-valued logic in combination with the classical implications.

Abstract The increasing need of the developed countries to carry out effective distance learning strategies has led to a great development of Internet‐based learning technologies (e‐learning). Despite its evident advantages, the expansion of e‐learning has been limited by the difficulty in reaching important social sectors, and also by the absence of mechanisms to fight the feeling of isolation of the users, which often leads them to abandoning the distance learning activities. This paper tackles these problems by introducing ATLAS, a framework for the development and deployment of multiuser t‐learning services (i.e. learning services over Interactive Digital TV). This framework is built around three major features: an architecture for the services that exploits the multimedia capabilities of the television, a communications infrastructure that promotes the establishment of virtual learning communities, and a development tool that allows services to be created with minimum programming knowledge. ATLAS has been designed by considering several features that make Interactive Digital TV quite different from the PC, advising against the direct translation of the models developed for the Internet. In particular, ATLAS adheres to the Multimedia Home Platform (MHP) standard, which is gaining worldwide acceptance as one of the technical solutions that will shape the future of Interactive Digital TV. Copyright © 2006 John Wiley & Sons, Ltd.

Abstract Nowadays, we are living in a time of important technological changes that affect our lives at home and our communication with the outside world. Among them, the developments in Interactive Digital TV (IDTV) and the smart home field can be considered as particularly important. Related to the former, the new Set‐Top Boxes (STBs) are not only a decoder for digital television broadcast but also an entry point to the Information Society and a suitable platform to support the execution of interactive applications. With regards to the latter, the Residential Gateways (RGs) combine different network technologies to allow the connection of different electronics devices and appliances at home, not only with each other but also with the Internet. Since there is no widespread consensus about the configurations and functions of the RGs, we propose to coordinate the two aforementioned worlds by extending the functionality of STBs to become a RG. Our proposal consists of merging the Multimedia Home Platform (MHP), one of the main standard frameworks for IDTV, with Open Service Gateway Initiative (OSGi), the most widely used open platform to set up RGs. To overcome the radically different nature of these specifications—the function‐oriented MHP middleware and the service‐oriented OSGi framework—we define a new kind of application, coined as XbundLET. This application is able to bridge the gap between the two frameworks and make their interaction feasible. We also show how this proposal has the potential to enable the production of scenarios that cannot currently be put into practice in a natural way. Copyright © 2006 John Wiley & Sons, Ltd.

In a totally formalized, iterative and incremental software process, each iteration usually implies identifying new requirements, adding them to the current model of the system, checking again the consistency and, in many cases, modifying the model to satisfy all the functional requirements. In this context, the ARIFS (Approximate Retrieval of Incomplete and Formal Specifications) methodology provides a suitable reuse environment (1) to classify, retrieve and adapt formal and incomplete requirements specifications and (2) to reuse the formal verification results linked to them. In this paper, we focus on the first goal describing the classification and retrieval tasks, which are based on functional similarities according to structural and semantic closeness. To this effect, we define four partial ordering relations among reusable components and several measures to quantify functional differences among them. By using these measures, we are able to offer an approximate and efficient retrieval, without formal proofs, and to predict adaptation efforts to satisfy the required functionality.

This paper presents several enhancements to ARIFS, a reuse environment that sets the foundations for reusing formal verification efforts in an iterative and incremental software process for the design of distributed reactive systems. A criterion based on generic components is added, together with a self-learning mechanism, to reduce the search space and maximize the probability of retrieving useful information. Besides, a formalization is given on how to apply verification tasks on a reduced number of states when the retrieved information is not enough for the user's intents. These enhancements are shown to improve both the effectiveness and the efficiency of ARIFS.

We adapt an analysis-revision cycle to SCTL-MUS methodology to support the modification and evolution of requirements specifications in a multiperspective environment. To illustrate the advantages of using our approach in the analysis and revision phases, we employ two viewpoints of a thermostat system. Both viewpoints are merged in order to reason over the properties of the composed system. The refinements over the merged model are transferred into each of the viewpoints and then into the requirements in which both are expressed. In this way, we obtain requirements refinements close to the system domain of each viewpoint, facilitating to the stakeholders the decision of what system requirements refinements must be included in the system requirements specification.

Achievement of quality in software design, while never easy, is made more difficult by the inherent complexity of hard real-time (HRT) design. Furthermore, timing requirements in HRT are by nature functional requirements, since system correctness depends on their fulfillment. Whereas the correctness dependence of the time imposes considering timing requirements from the early stages of the production process, complexity enforces a lifecycle model which fits in with requirements change and splits complexity by means of an incremental and iterative structure. Taking these aims as a starting point, this paper introduces SCTL/MUS-T methodology as supporting HRT design in a formalized and incremental way.

This paper describes how ARIFS tool (Approximate Retrieval of Incomplete and Formal Specifications) provides a suitable reusing environment to classify, retrieve and adapt formal and incomplete requirements specifications. Both classification and retrieval tasks are based on functional similarities according to structural and semantic closeness. To this effect, we define four partial orderings among reusable components and different measures to quantify functional differences among them. By using these measures we are able to offer an approximate and efficient retrieval, without formal proofs, and to predict adaptation efforts to satisfy the required functional specification. This paper focus on semantic similarities as they are more remarkable in vertical reuse, that is, the reuse of software within same domain or application area.

The possibility of verifying systems during any phase of the software development process is one of the most significant advantages of using formal methods. Model checking is considered to be the broadest-used formal verification technique, even though a great quantity of computing resources are needed to verify medium-large and large systems. As verification is present over the whole software process, this amount of resources is more critical in incremental and iterative life-cycles. Our proposal focuses on reusing incomplete models and their verification results - which are obtained from a model-checking algorithm - in order to improve this kind of life-cycle. Making good use of these previous verification results can reduce the formal verification costs by minimizing the set of requirements and the set of system states where the properties must be verified. The unspecification that is inherent to incomplete systems is used to provide an approximate and content-oriented retrieval which is supplemented by suggestions to match the desired specifications.