While students are often passionate about their chosen fields, they often have limited awareness of the profound impact of AI technologies on their professions. In order to advance efforts in building subject-relevant AI literacy among undergraduate students studying Computer Science and non-Computer Science (Criminal Justice and Forensic Science) it is imperative to engage in rigorous efforts to develop and study curricular infusion of Artificial Intelligence topics. Using a Design-Based Research model, the project team and the external evaluators studied the first iteration of the module development and implementation. Using data collected through surveys, focus groups, critical review, and reflection exercises the external evaluation team produced findings that informed the project team in revising and improving their materials and approach for the second iteration. These efforts can help educators and the AI module developers tailor their AI curriculum to address these specific areas, ensuring that students develop a more accurate understanding of applications of AI in their future career field.

The article outlines a contemporary method for creating software for multi-processor computers. It describes the identification of parallelizable sequential code structures. Three structures were found and then carefully examined. The algorithms used to determine whether or not certain parts of code may be parallelized result from static analysis. The techniques demonstrate how, if possible, existing sequential structures might be transformed into parallel-running programs. A dynamic evaluation is also a part of our process, and it can be used to assess the efficiency of the parallel programs that are developed. As a tool for sequential programs, the algorithms have been implemented in C#. All proposed methods were discussed using a common benchmark.

The recent COVID-19 pandemic accelerated the world's digitalization including transformation of traditional auctions. Although buyers cannot examine an item in online auctions, they become a more popular option. They are more convenient since buyers can participate from all around the world. Additional advantage is that the possibility to make auctions more anonymous. Specifically, it may be crucial for the user to keep their interest in the commodity hidden from other buyers and even the seller. This article explores the problem of anonymization in web services by using the example of anonymous online auctions. A system for anonymous, blockchain-based online auctions using zero-knowledge proof is proposed. The system enables a party to attend an auction anonymously digitally isolated from other competitors and the sellers. The system consists of a smart contract on a blockchain and a decentralized web application that facilitates zero-knowledge proof calculation and interactions with the smart contract.

The paper presents a modern approach to software development for multi-processor platforms. It focuses on sequential code structures that can be parallelized. Several structures were identified and then analyzed in detail. Such static analysis led to the algorithms determining whether specific pieces of code can be parallelized. The algorithms show how existing sequential structures can be converted to programs executed in parallel, if feasible. Our methodology also includes a dynamic evaluation that can determine the effectiveness of the generated parallel programs. The algorithms have been implemented as a tool for sequential programs in C#. Future solutions were discussed.

Reports of progress in research into Artificial Intelligence (AI) and its applications are accumulating very rapidly. Specifically, Machine Learning (ML) applications based on large data sets have moved to the forefront of innovations in the field. New ML models have led to the adoption of AI in different disciplines. The development of the most recent large language models has created so much interest that it might mean a revolution in using of AI. Some make a stronger claim that it is a turning point in human civilization's history, and we have started the AI age after replacing the obsolete in many aspects of Information Age applications. One of the immediate challenges is how to use AI and ML responsibly with proper protection for humans and human society. In this paper, we report on our efforts in introducing trustworthiness of ML in college curricula and what factors influence AI-supported decision making. The main goal is to allow students to gain an understanding not only of concepts but also of the limitations of AI. This will help in their participation in our society of the AI Age. The process of AI democratization needs to be established to control the growth of ML use and understand the human dangers of various types of data-driven modeling approaches in AI.

Designing and implementing Web Services constitutes a large and constantly growing part of the information technology market. Web Services have specific scenarios in which distributed processes and network resources are used. This aspect of services requires integration with the model checkers. This article presents the experimentation framework in which services can be specified and then formally analyzed for deadlock-freedom, achievement of process goals, and similar features. Rybu4WS language enriches the basic Rybu language with the ability to use variables in processes, service calls between servers, new structural instructions, and other constructions known to programmers while remaining in line with declarative, mathematical IMDS formalism. Additionally, the development environment allows simulation of a counterexample or a witness - obtained as a result of the model checking - in a similar way to traditional debuggers.

With the recent successes of research in Artificial Intelligence (AI), specifically Machine Learning (ML), infusion of AI and ML concepts and use of tools can help increase the responsible adoption of AI and ML in different disciplines. We report on the design of a workshop on ML, results from the evaluation of the workshop, and suggests topics and pedagogical approaches that may be adopted for disseminating the core concepts of ML which are among the most prevalent data-driven modeling approaches in AI. The workshop individually targeted a diverse range of participants including college and university faculty members from different disciplines at 2-and-4 year institutions. The materials of the workshop were made publicly available. Future workshops and educational modules building on this work will be able to infuse knowledge of the frontiers of AI and problems & benefits.

Selecting peptides that bind strongly to the major histocompatibility complex (MHC) for inclusion in a vaccine has therapeutic potential for infections and tumors. Machine learning models trained on sequence data exist for peptide:MHC (p:MHC) binding predictions. Here, we train support vector machine classifier (SVMC) models on physicochemical sequence-based and structure-based descriptor sets to predict peptide binding to a well-studied model mouse MHC I allele, H-2Db. Recursive feature elimination and two-way forward feature selection were also performed. Although low on sensitivity compared to the current state-of-the-art algorithms, models based on physicochemical descriptor sets achieve specificity and precision comparable to the most popular sequence-based algorithms. The best-performing model is a hybrid descriptor set containing both sequence-based and structure-based descriptors. Interestingly, close to half of the physicochemical sequence-based descriptors remaining in the hybrid model were properties of the anchor positions, residues 5 and 9 in the peptide sequence. In contrast, residues flanking position 5 make little to no residue-specific contribution to the binding affinity prediction. The results suggest that machine-learned models incorporating both sequence-based descriptors and structural data may provide information on specific physicochemical properties determining binding affinities.

IoT networks continuously evolve and require new theoretical and practical studies. Complex cooperation between IoT devices, based on interaction with their internal states especially needs to be based on new significant scientific solutions. To pursue this goal we propose a dual formalism for a distributed systems being IoT networks. We refer to it as the Integrated Model of Distributed Systems (IMDS), implemented in the Dedan framework. In this dual but integrated framework, the two views of a distributed system are available: the server view of cooperating modules or the agent view of migrating threads. The Dedan framework automatically finds deadlocks and checks distributed termination in a modeled system, observed in servers communication or in sharing resources by agents. Partial deadlocks/termination are also identified, i.e., some activities may be performed in a system that is partially deadlocked/terminated. Automated verification supports the rapid development of IoT protocols. In this paper, we also discuss the problem of how the exhaustive search in the process of deadlock detection can be improved by probabilistic search using machine learning.

In this paper, we extended previous studies of cooperating autonomous robots to include situations when environmental changes and changes in the number of robots in the swarm can affect the efficiency to execute tasks assigned to the swarm of robots. We have presented a novel approach based on partition of the robot behaviour. The sub-diagrams describing sub-routs allowed us to model advanced interactions between autonomous robots using limited number of state combinations avoiding combinatorial explosion of reachability. We identified the systems for which we can ensure the correctness of robots interactions. New techniques were presented to verify and analyze combined robots’ behaviour. The partitioned diagrams allowed us to model advanced interactions between autonomous robots and detect irregularities such as deadlocks, lack of termination etc. The techniques were presented to verify and analyze combined robots’ behaviour using model checking approach. The described system, Dedan verifier, is still under development. In the near future, timed and probabilistic verification are planned..

In this paper, we describe our protein folding research with the goal of improving protein model scoring by grouping of protein models and using an interpreter for machine learning (ML). The traditional approach is to use a handful of popular ML algorithms, such as Support Vector Machines (SVM), Random Forest and Neural Networks that are trained on a whole set of models. Our approach is to group the protein models and train the ML algorithms on each group separately. Our framework can be generalized to other application of ML where there is a strong diversification of data set. In this paper, we describe results of comparison of traditional vs. our grouping approach showing that some improvement in the scoring of protein models can be achieved. To further improve the scoring, an interpreter for machine learning is used. The interpreter is based on Local Interpretable Model-Agnostic Explanations (LIME) tool. In this paper it is used to determine feature vector for each group of protein models. Different feature vectors are then used for ML training on different groups of protein models allowing us to improve the ML algorithms. In addition, interpreter of ML can be used in the future to provide feedback for the process of protein models generation.

In recent years Artificial Intelligence (AI) and Machine Learning (ML) have emerged from academic labs and become prominent drivers of innovation in the high-tech industry. The number of jobs in this area has rapidly increased along with research output from industry and the commercialization of that research. It is widely accepted that the changes resulting from these advances will shape society. Diversity in these fields must be increased not only to get people from underrepresented populations into these lucrative jobs but also to have a positive impact by expecting that a more diverse workforce will ensure the fairness of data-driven decisions made by AI and ML algorithms, an issue that has come under scrutiny. The work described here is a result of ongoing efforts to modernize AI and ML courses, and to make its techniques an integral part of the software engineering capstone course at our educational institutions. We report on how the courses and the practice of software engineering have adopted cloud based platforms where we gain the benefit of creating virtual machines and containers for necessary software stacks, the pedagogical benefits of using open-source software that enable blending of markup text, code and output from code within the same document. Information about the choice of software libraries to help students produce code and perform experiments on data at an early stage is an important topic that is included in the discussion. We list of examples of where we have leveraged existing student interest in application of AI and ML, to motivate the work on projects. The defense and intelligence community of the US government are invested in a diverse talent pool in this area. Efforts in specialized certification, and faculty-student visits to government labs are described in this work.

Environmental changes, failures, collisions or even terrorist attacks can cause serious malfunctions of the delivery systems. We have presented a novel approach improving resilience of Autonomous Moving Platforms AMPs. The approach is based on multi-level state diagrams describing environmental trigger specifications, movement actions and synchronization primitives. The upper level diagrams allowed us to model advanced interactions between autonomous AMPs and detect irregularities such as deadlocks live-locks etc. The techniques were presented to verify and analyze combined AMPs' behaviors using model checking technique. The described system, Dedan verifier, is still under development. In the near future, a graphical form of verified system representation is planned.

This paper discusses new techniques to enhance Automated Transit Networks (ATN, previously called Personal Rapid Transit - PRT) based on Artificial Intelligence tools. The main direction is improvement of the cooperation of autonomous modules that use negotiation protocols, following the IoT paradigm. One of the goals is to increase ATN system throughput by tuning up autonomous vehicles cooperation. Machine learning (ML) was used to improve algorithms designed by human programmers. We used existing controls corresponding to near-optimal solutions and built refinement models to more accurately relate a system's dynamics to its performance. A mechanism that mostly influences ATN performance is Empty Vehicle Management (EVM). The algorithms designed by human programmers was used: calls to empty vehicles for waiting passengers and balancing based on reallocation of empty vehicles to achieve better regularity of their settlement. In this paper we discuss how we can improve these algorithms (and tune them to current conditions) by using ML to tailor individual behavioral policies. Using ML techniques was possible because our algorithm is based on a set of parameters. A number of weights and thresholds could be tuned up to give better decisions on moving empty vehicles across the track.

Concurrent software for engineering computations consists of multiple cooperating modules. The behavior of individual modules is described by means on state diagrams. In the paper, the constraints on state diagrams are proposed, allowing for the specification of designer's intentions as to the synchronization of modules. Also, the translation of state diagrams (with enforcement constraints) into Concurrent State Machines is shown, which provides formal framework for the verification of inter-module synchronization. An example of engineering software design based on the method is presented.

The case study analyzed in the report involves the behavioral specification and verification of a three-stage pipeline consisting of mutually concurrent modules which also compete for a shared resource. The system components are specified in terms of Concurrent State Machines (CSM) and the verification technique used is the temporal model checking in the COSMA environment.

An engineering design process may involve software modules that can executed concurrently. Concurrent modules can be very easily subject to some synchronization errors. This paper discusses verification process for such engineering software. We present a method for verification that requires several steps. First, the state diagram models are constructed that describe the design iterations and interactions with the designer. Next, the state diagram models are transformed into concurrent state machines (CSM). After that, the CSM models are analyzed in order to verify their correctness. In this phase, the modifications are performed in necessary. In the last phase the code is generated. The tools to support our method can be called new concurrent CASE tools. Using these tools the engineering software can be created that is verified for correctness in respect to concurrent execution.

In this paper we focus on collaborative computer programming in new environments. The ontology-based approach is used as an important support for programming. It creates a common framework of reference for discussion to all participating programmers. In our experiments ontology was used to describe classification of programming components. We defined several models of cooperative ontology-based software development.

In this paper, we are proposing to enhance undergraduate student research by including significant comparative analysis activities. Our approach to implement these activities is to carry out two different research projects for two groups of students that have a common theme. We refer to them as synergistic projects. The first of these synergetic projects is to leverage vision-based algorithms to conduct autonomous target tracking. The second is to advance the solutions in swarm robotics for the NASA space mission. Significant value can be added to student research activities by involving two groups of students working on two different projects in close cooperation. It can increase a depth of understanding of the problems by contrasting the solutions and therefore creating a more solid framework for student research in computer science. Such a framework makes the research more effective and attractive by exposing alternative solutions, alternative evaluations for solutions, and limits for solutions.

This paper addresses the challenge of measuring security, understood as a system property, of cyberphysical systems, in the category of similar properties, such as safety and reliability. First, it attempts to define precisely what security, as a system property, really is. Then, an application context is presented, in terms of an attack surface in cyberphysical systems. Contemporary approaches related to the principles of measuring software properties are also discussed, with emphasis on building models. These concepts are illustrated in several case studies, based on previous work of the authors, to conduct experimental security measurements.