This innovative practice full paper introduces the design, organization, and evaluation of two one-week summer camps to introduce multi-disciplinary engineering technology and programming to high school students. This program is designed to increase students' interests and knowledge of multi-disciplinary engineering and computing, foster collaboration, and build community. By engaging in our program, students not only think critically and enhance their problem-solving skills but also develop foundational proficiency in engineering and computational thinking. This crucial skill set is recognized as essential in the 21st century, opening doors to enriching engineering capabilities and creating diverse opportunities for pursuing careers in multiple engineering fields. This paper introduces the organizational structure, coordination strategies, core curriculum instructions, and the program assessment result which demonstrates a substantial improvement in knowledge and increased interest in computing and engineering across all participant cohorts. The primary objective of this paper is to furnish a detailed guide, equipping institutions with the essential information required to successfully host similar summer programs. Furthermore, it aims to catalyze endeavors geared towards enhancing young students' participation in the fields of computing and engineering.

While the mixed-criticality (MC) approach is naturally suited for multi-processor (or multi-core) systems, scheduling MC tasks on these platforms is much more complex than in the non-MC case. Here, we improve one of the few approaches that explicitly consider criticality information in scheduling the bus access by allowing a more flexible time allocation to the tasks.

This Innovative Practice Full Paper presents our design of teaching computer programming for middle and high school students during an one-week Summer camp for the past five years, with an interruption in the Summer of 2020 due to the Covid-19 pandemic. Many researchers believe that good Summer camps can improve many students' educational and career development outcomes. Teachers and administrators are increasingly promoting Summer camp opportunities for introducing programming skills to middle and high school students. The motivation of our program is to offer hands-on projects for middle and high school students to increase their interests and knowledge in computing to meet the growing demand. Like some Summer coding camps, we picked Scratch as the programming language (designed and offered for free by the Massachusetts Institute of Technology) for the students to learn important mathematical and computer programming concepts. In addition, the students learn how to think and reason creatively, reason systematically, and work collaboratively, while also having fun during the one-week Summer camp. For the students already familiar with Scratch, the instructor exposed students to basic concepts of Java programming language, such as Java virtual machine, computer memory, data representation, primitive data types, casting, arithmetic, and relational operators, as well as the assignment, selection and printing statements. This article presents our findings from Summer camps organized in 2018 and 2022. Our conclusion is that all students showed a better understanding of programming concepts and confidence in computing. In the upcoming paper sections, we will describe details about how we made one-week camps to be unique compared to other similar camps. One element of our own approach is to teach in an effective and innovative using an interactive teaching approach. For example, when we designed the lecture notes, we imagine that we are students taking for the first time a computer programming course. In addition, we designed simple programming exercises for the students to solve immediately. The instructors and Teaching Assistants promptly checked the solution and award the students with stars for completing the work. This environment was very well received because it was viewed as a student collegiate competition instead of a race against time. Besides learning about computer programming, we adopted during Summer camps several strategies like those enumerated earlier to enrich our camps, as well as social events, career and professional development, and academic exposure. Our findings indicate that these additional activities proved to be beneficial to our students attending the Summer camps.

This Innovative Practice Full Paper introduces a comparative study of utilizing several popular educational robotics to introduce engineering and computing concepts to middle school and high school students to increase their interests and knowledge in engineering and computing. Using robotics is a great way to introduce engineering and computing concepts in a fun and interactive way. There are several popular educational robotic kits available, e.g., Lego EV3, VEX robotics, SparkFun Inventor's Kit, Raspberry Pi, SeaPerch underwater robotics, etc. All these robotics are great options for creating fun and engaging projects that encourage creativity and problem-solving skills for middle school and high school students. While they all have their unique features and benefits, there are some similarities and differences that can help with choosing the right tool for a specific group of students at different ages and skill levels. The motivation of this study is to provide detailed information and a comparative study of utilizing several popular educational robotics to teach engineering and computing concepts to middle school and high school students for those who are interested in organizing similar programs at their institutions to prompt the effort to increase participation in engineering and computing fields. Studies have proved that by introducing engineering and computing concepts early on, students can develop an interest in these fields and pursue them in the future.

This innovative Practice Full Paper establishes two one-week summer camps to introduce fundamental engineering and programming concepts to middle-school and high-school students using the SparkFun Inventor’s Kit, Scratch, Makers Empire 3D Design Software, and Java. The SparkFun Inventor’s Kit is a great way to introduce electronics and programming concepts to students who have little, no previous programming, or circuit construction experience. During the one-week summer camp, students were introduced to the Arduino-based SparkFun Inventor’s Kit as the hardware platform, along with Arduino’s Integrated Design Environment (IDE) for programming. Scratch was used to teach fundamental programming concepts such as arithmetic operations, strings, conditional statements, and loops. The motivation of our program is to offer hands-on engineering and programming experiences for middle-school and high-school students to increase their interests and knowledge in engineering and computing to promote student participation to meet the growing demand. Our program is unique in several ways: First, we developed several hands-on projects to integrate topics related to engineering and computing to help students develop and build skills of critical thinking, problem-solving, and invention. Second, we used several teaching tools, e.g., SparkFun Inventor’s Kit, Scratch, Makers Empire 3D Design Software, and Java to enrich students’ learning experience, while other programs used only one of those teaching tools. Third, we adopted several strategies to enrich our program, such as social encouragement, academic exposure, career perception, and social learning, which have shown beneficial effects on student learning in the literature to improve learning outcomes. Fourth, we also provided students the opportunity of a campus tour to help students get familiar with college life. Fifth, we organized team-building activities outside the classroom to build skills of effective collaboration and communication. Participants obtained a better understanding of principle programming, engineering concepts, and confidence in engineering and computing. The assessment results showed a significant increase in knowledge and interest in engineering and computing. This paper introduces the detailed information about our program organization, coordination, core curriculum design, and program assessment for organizing similar summer camps at other institutions and further prompts the effort to increase participation in engineering and computing fields.

Our poster covers the organization, curriculum design, and assessment of two summer camps we organized in Summer 2021 to teach middle school students fundamental programming concepts to increase their knowledge and interests in computer science. We designed several hands-on projects using the SparkFun Inventor's Kit, Scratch, and Makers Empire 3D Design Software. Scratch was used to teach fundamental programming concepts such as arithmetic operations, strings, conditional statements, and loops. The SparkFun Inventor's Kit provides a powerful and in-depth programming experience for middle school students. The Mission to Mars Design Challenge Activity utilized Makers Empire 3D Design Software and Scratch and allowed students to explore and determine the specific needs of a mission to Mars while challenging them to brainstorm, design, and create an invention or new tool. Those hands-on programming experiences helped students to develop and build creative confidence, design thinking skills, and problem-solving skills. Our program assessment results showed that camp participants increased their knowledge and interests in subjects related to programming and computer science. Our poster provides detailed information about organizing similar summer camps at other institutions to increase general participation in computer science.

This Innovative Practice Full Paper introduces the design, organization, and assessment of a one-week summer camp geared towards integrating programming and engineering concepts using Raspberry Pi and Scratch for incoming 8th-grade female students to increase their interest and knowledge of Computing and Engineering. The purpose of offering this camp is to increase female participation in the computing and engineering fields to close the gender gap. This summer camp focused its efforts on teaching incoming 8th-grade female students the fundamentals of programming skills and engineering concepts. We taught our camp participants to use Raspberry Pi to build systems that explore fundamental programming and engineering concepts and develop engineering skills. Raspberry Pi provides a general programming environment with numerous interfaces to allow direct control of the hardware. This paper describes the organization, coordination, and core curriculum instructions that integrate programming and engineering concepts taught in each hands-on session and discusses the program assessment results. Our program assessment results showed that all camp participant cohorts increased their knowledge and interests in computing and engineering. This paper intends to provide all the information needed to host similar summer camps at other institutions, and further prompt the effort to increase female participation in computing and engineering fields.

Detecting heart diseases has been a research interest for centuries. Many of these approaches are based on heartbeat analysis using a stethoscope and some of these are digitally analyzed. In an ordinary system, doctors use an acoustic stethoscope to detect any aberration in the heartbeat and predict atypical conditions of the human heart. One major problem is that the frequency range and intensity of the heart sounds are flat as well as the sound may contain noise. Hence, even a cardiac specialist doctor may encounter difficulties to analyze the heart sound perfectly. This paper describes a new methodology to detect heart diseases by examining heart sounds in real-time. We consider the guts sound as our input data. Our methodology uses a deep learning approach to determine whether a patient has any disease or is healthy. To achieve that, we integrated an electronic stethoscope and a software solution known as a heartbeat audio classifier. Our proposed system solution should be able to differentiate normal heartbeats and heart murmurs with a prediction of probable heart problem type in real-time. We believe our approach assists in reducing the cardiac arrest rate.

The concept of graceful degradation in mixed-criticality real-time systems is still struggling to reach a widely accepted, global view. Numerous results have emerged in this field during the last years, but there is still a lot of work to do. This paper comes with an addition to a recent work [2] in the field of scheduling in semi-clairvoyant systems: it introduces a new criterion for determining which low criticality jobs should be switched upon a system criticality mode transition.

This Innovative Practice Full Paper discusses a STEM academy that used SeaPerch and Scratch as engaging hands-on approaches to teach seventh grade middle school girls engineering skills, scientific principles, and programming concepts to increase their knowledge and interest in science, technology, engineering, and mathematics (STEM). Adding diversity to the STEM workforce and increasing enrollment in STEM degrees is critical for fulfilling the needs of our modern economy. Today, many organizations/institutions are preparing future workers for the modern workforce by implementing summer camps/academies to engage students in STEM disciplines at a young age. Exposing young students to the critical thinking and reasoning skills that are intrinsic to STEM disciplines can help to alleviate or even combat the decline of students in STEM careers. We have developed an academy to demonstrate STEM concepts to 7th grade girls. Our STEM academy differs from others in several ways: First, it was for 7th grade girls only, creating a non-competitive social learning opportunity, to improve female participation. Second, we hired female instructors and invited female professionals from local industries to assist the academy by serving as mentors and role models for the participants. Third, it introduced STEM concepts and principles to the girls. Fourth, it adopted social learning, e.g., buddy system, to help the girls to learn better. A formal assessment of the 2018 academy found that the academy's participants experienced a significant increase in knowledge and interest in STEM. This paper describes the organization, coordination, content, and assessment of the STEM academy. It describes how the academy was organized and taught, which includes a brief description of the instructional materials, the concepts taught in each hands-on session, how the academy was assessed, the assessment results, the first-year experience of conducting the STEM academy, and lessons learned. This paper provides all the information needed for others to host similar academies and motivate the effort to increase female participation in STEM careers.

This Innovative Practice Full Paper discusses a coding/programming academy that used games and robotic programming as engaging hands-on approaches to teach 6thgrade (the first grade in secondary education in USA) females coding/programming concepts to increase their knowledge and interest in computer science. Careers in computer science continue to grow, but fewer women than men are even considering these careers. Increasing participation of women in coding/programming is necessary to meet the growing demand for computing professionals to develop a diverse workforce. Today, many organizations are implementing programming coding/programming academies/camps that attempt to engage students in computer science, at an early age, by exposing them to fun and interesting computer science skills in coding/programming. We have developed a coding/programming academy that uses educational robotics and hands-on game applications to demonstrate computing concepts to young females. To address pressing equity issues of the lack of females in computer science careers, the goal of this summer coding/programming academy was to educate and empower young females, at an early age, to discover computer science careers, which has been one of the first attempts to establish a coding/programming academy for females in our region. Our coding/programming academy differs from others in several ways. First, it was for 6th-grade females only, to take advantage of preferences of noncompetitive and social learning opportunities, in order to improve female participation. Second, we hired female instructors and invited female professionals from local industries to assist the academy by serving as mentors. Third, it introduced both robotic and game coding/programming to the females. Fourth, it adopted social learning, e.g., pair programming. A formal assessment of the 2018 academy found that the academy's female participants experienced a significant increase in knowledge and interest in computer science. This paper describes the organization, coordination, content, and assessment of the coding/programming academy. It describes how the academy was organized and taught, which includes a brief description of the instructional materials, the concepts taught in each hands-on session, how the academy was assessed and the assessment results, and the first-year experience of conducting the coding/programming academy, and lessons learned. The intent of this paper is to provide all the information needed for others to host similar academies and further prompt the effort to increase female participation in computer science careers.

Tasks' scheduling has always been a central problem in the embedded real-time systems community. As in general the scheduling problem is NP-hard, researchers have been looking for efficient heuristics to solve the scheduling problem in polynomial time. One of the most important scheduling strategies is the Earliest Deadline First (EDF). It is known that EDF is optimal for uniprocessor platforms for many cases, such as: non-preemptive synchronous tasks(i.e., all tasks have the same starting time and cannot be interrupted), and preemptive asynchronous tasks (i.e., the tasks may be interrupted and may have arbitrary starting time). However, Mok showed that EDF is not optimal in multiprocessor platforms. In fact, for the multiprocessor platforms, the scheduling problem is NP-complete in most of the cases where the corresponding scheduling problem can be solved by a polynomial-time algorithm for uniprocessor platforms. Coffman and Graham identified a class of tasks for which the scheduling problem can be solved by a polynomial time algorithm, that is, two-processor platform, no resources, arbitrary partial order relations, and every task is nonpreemptive and has a unit computation time. Our paper introduces a new non-trivial and practical subclass of tasks, called urgent tasks. Briefly, a task is urgent if it is executed right after it is ready or it can only wait one unit time after it is ready. Practical examples of embedded real time systems dealing with urgent tasks are all modern building alarm systems, as these include urgent tasks such as `checking for intruders', `sending a warning signal to the security office',`informing the building's owner about a potential intrusion', and so on. By using propositional logic, we prove a new result in schedulability theory, namely that the scheduling problem for asynchronous and preemptive urgent tasks can be solved in polynomial time.

Semantic caching is a dynamic caching strategy which deals with not only exact but also inexact similar queries. In this manner, each query will be carefully analyzed by the cache manager to identify the part that can be found in the cache from the part that needs to be retrieved from the server. This trimming process not only speeds up information retrieval but also saves on communication cost especially for mobile and wireless devices. Therefore, query trimming is a key problem in mobile and wireless environment, and devices in this environment have limited connection time, bandwidth, and battery power. However, the existing methods for query trimming have a number of limitations such as, inefficiency in time, space and the complexity of the algorithm used for trimming. These factors restrict the applicability of semantic caching for many applications. In this paper we investigate the shortcomings of query trimming process and propose a new solution to improve this process.

Abstract Both specification and verification of business processes are gaining more and more attention in the field. Most of the existing works in the last years are dealing with important, yet very specialized, issues. Among these, we can enumerate compensation constructs to cope with exceptions generated by long running business transactions, fully programmable fault and compensation handling mechanism, web service area, scope-based compensation and shared-labels for synchronization, and so on. The main purpose of this paper is to present a semi-automatized framework to describe and analysebusiness processes. Business analysts can now use a simple specification language (e.g.,BPMN[Obj06]) to describe any type of activity in a company, in aconcurrentandmodularfashion. The associated programs (e.g.,BPDs [Obj06]) have to be executed in an appropriate language (e.g.,BPEL4WS[ACD+03]). Much more, they have to beconfirmed to be sound, via some prescribed (a priori) conditions. We suggest how all the issues can be embedded in aunifying computer tool. We link our work with similar approaches and we justify our particular choices (besidesBPMNandBPD): theTLA+ language for expressing the imposed behavioural conditions andPetri Nets([EB87], [EB88]) to describe an intermediate semantics. In fact, we want to manage in an appropriate way the general relationship diagram (Fig. 1). Examples and case studies are provided.

Embedded and real-time systems are increasingly common and complex, requiring formal specification and verification in order to guarantee their satisfaction of desirable safety and timing requirements. Real-Time Logic (RTL) has been used to capture both the specification (denoted by SP) of a real-time system and the desirable safety assertions (denoted by SA) with respect to this system specification. A verification procedure then determines whether the safety assertions hold with respect to the system specification. However, the satisfiability problem for RTL (i.e., "Can SP \rightarrow SA hold?”), as well as for other first order logics, is undecidable. Consequently, efforts have been focused on identifying nontrivial classes of formulas sufficiently practical for describing industrial real-time systems for which the verification and debugging can be done via efficient heuristics. One such class of formulas is the so-called path RTL. The first contribution of this paper is to extend the existing path RTL class without sacrificing the time complexity of the traditional path RTL heuristic for verification. This implies that we can specify and verify real-time systems, which we were unable to do using the existing path RTL, in the extended path RTL. For real-time systems with large specifications, there is a lot of room for improvement in the algorithms used for verification and debugging. The second contribution of this paper is an efficient method to perform verification and debugging of real-time systems specifications using decomposition techniques. Our idea is to decompose the constraint graph, used in existing approaches, into independent subgraphs so that it is no longer necessary to analyze the entire specification at once, but rather its individual and smaller components. However, none of the above heuristics necessarily finds an “optimal implication.” After verifying SP \rightarrow SA and deploying the system implementing SP, performance changes as a result of power saving, faulty components, and cost saving in the processing platform for the tasks specified in SP affect the computation times of the specified tasks. This leads to a different but related SP, which would violate the original SP \rightarrow SA theorem if SA remains the same. It is desirable, therefore, to determine an optimal SP with the slowest possible computation times for its tasks such that the SA is still guaranteed. This is clearly a fundamental issue in the design and implementation of highly dependable real-time/embedded systems. The third contribution of this paper tackles this fundamental issue by describing a new method for relaxing SP and tightening SA such that SP \rightarrow SA is still a theorem. We have implemented this method in the Java-based DEVO-RTL tool and tested it on several industrial real-time systems. Experimental results show that only about 10 percent of the running time of the heuristic for the verification of SP \rightarrow SA is needed to find an optimal theorem.

Formal specification and verification are critical to the development of safe real-time and embedded systems, which have become increasingly complex. Real-Time Logic (RTL) has been used to describe the specification and safety asser- tion of real-time systems. However, the satisfiability prob- lem for RTL, as well as other first-order logics, is unde- cidable. There exist already non-trivial fragments of RTL, like path RTL and extended path RTL, for which the veri- fication can be done efficiently. The key idea used by these RTL fragments was the so-called constraint graph. The con- straint graph can express dependencies between two events, but cannot describe dependencies between three or more events. This paper presents a larger class than existing frag- ments of RTL for which the verification problem can also be solved efficiently. Our new class is called Linear Real- Time Logic (LRTL) and includes the existing decidable RTL fragments like path RTL and extended path RTL. The LRTL class is able to express any linear timing constraint with an arbitrary number of events variables (e.g., between three or more events). The main ingredient of the LRTL class is the use of matrices instead of the constraint graph, as a more powerful data structure capable of performing the conver- sion from RTL to a propositional formula. The unsatisfi- ability of the propositional formula will ensure the safety and feasibility of the given real-time system. Experimental results show that the execution times for LRTL are better than the systems expressed in extended path RTL, and com- parable with those expressed in path RTL.

Recursive programs may require large numbers of procedure calls and stack operations, and many such recursive programs exhibit exponential time complexity, due to the time spent re-calculating already computed sub-problems. As a result, methods which transform a given recursive program to an iterative one have been intensively studied. We propose here a new framework for transforming programs by removing recursion. The framework includes a unified method of deriving low time-complexity programs by solving recurrences extracted from the program sources. Our prototype system, APTSR1, is an initial implementation of the framework, automatically finding simpler "closed form" versions of a class of recursive programs. Though in general the solution of recurrences is easier if the functions have only a single recursion parameter, we show a practical technique for solving those with multiple recursion parameters.

Real-time logic (RTL) is useful for the verification of a safety assertion SA with respect to the specification SP of a real-time system. Since the satisfiability problem for RTL is undecidable, there were many efforts to find proper heuristics for proving that SPrarrSA holds. However, none of such heuristics necessarily finds an "optimal implication". After verifying SPrarrSA, and the system implementing SP is deployed, performance changes as a result of power-saving, faulty components, and cost-saving in the processing platform for the tasks specified in SP affect the computation times of the specified tasks. This leads to a different but related SP, which would violate the original SPrarrSA theorem if SA remains the same. It is desirable, therefore, to determine an optimal SP with the slowest possible computation times for its tasks such that the SA is still guaranteed. This is clearly a fundamental issue in the design and implementation of highly dependable real-time/embedded systems. This paper tackles this fundamental issue by describing a new method for relaxing SP and tightening SA such that SPrarrSA is still a theorem. Experimental results show that less than 20% overhead of the running time of the algorithm for the verification of SPrarrSA is needed to find an optimal theorem

Embedded and real-time systems are increasingly common and complex, requiring formal specification and verification in order to guarantee their satisfaction of desirable safety and timing requirements. Real-Time Logic (RTL) has been used to capture both the specification of a real-time system and the desirable safety assertions with respect to this system specification. A verification procedure then determines whether the safety assertions hold with respect to the system specification. However, the satisfiability problem for RTL, as well as for other first-order logics, is undecidable. Consequently, efforts have been focused on identifying non-trivial classes of formulas sufficiently practical for describing industrial real-time systems for which the verification and debugging can be done via efficient heuristics. One such class of formulas is the so-called path RTL. The first contribution of this paper is to extend the existing path RTL class without sacrificing the time complexity of the traditional path RTL heuristic for verification. This implies that we can specify and verify real-time systems, which we were unable to do using the existing path RTL, in the extended path RTL. For real-time systems with large specifications, there is a lot of room for improvement in the algorithms used for verification and debugging. The second contribution of this paper is an efficient method to perform verification and debugging of real-time systems specifications using decomposition techniques. Our idea is to decompose the constraint graph, used in existing approaches, into independent subgraphs so that it is no longer necessary to analyze the entire specification at once, but rather its individual and smaller components. We have implemented this method in the Java-based DEVA-RTL tool and tested it on several industrial real-time systems.

Real-time logic (RTL) is useful for the verification of a safety assertion with respect to the specification of a realtime system. Since the satisfiability problem for RTL is undecidable, the systematic debugging of a real-time system appears impossible. A first step toward this challenge was presented. With RTL, each prepositional formula corresponds to a verification condition. The number of truth assignments of a prepositional formula can help us determine the specific constraints which should be added or modified to get the expected solutions. This paper solves an even more challenging problem specified as future work, namely, the embedding and the integration of our debugger in autonomous systems which generate real-time control plans on-the-fly, since these specifications must meet timing constraints, but without human interaction. The idea is to consider in advance all the necessary information, such as the designer's guidance. We have implemented a tool (called ADRTL) that is able to perform automatic debugging. The confidence of our approach is high as we have successfully evaluated ADRTL on several existing industrial-based applications.

On current superscalar processors, performance and power issues cannot be decoupled for designers. Extensive simulations are usually required to meet both power and performance constraints. This paper describes an integrated performance and power analytical model. The model's performance and power results are in good agreement with detailed simulations, previous models and physically measured results. For designers, the model enables quick and flexible explorations into a subset of even entire huge parameter space of more than 15 workload and architectural parameters plus leakage power, feature sizes, clock and voltage.

Real-time logic (RTL) (F. Jahanian et al., 1986, 1987, F. Wang et al., 1994) is useful for the verification of a safety assertion with respect to the specification of a real-time system. Since the satisfiability problem for RTL is undecidable, the systematic debugging of a real-time system appears impossible. This paper provides a first step towards this challenge. With RTL, each propositional formula corresponds to a verification condition. The number of truth assignments of a propositional formula helps to determine the timing constraints which should be added or modified to the system's specification. We have implemented a tool (called SDRTL, (S. Andrei et al., 2004)) that is able to perform systematic debugging. The confidence of our approach is high as we have evaluated SDRTL on several existing industrial-based applications.

Circuit testing is the most significant cost in modern chip design and production. Due to the complexity in terms of millions of gates, manufacturers often have to truncate test patterns to make the testing feasible on ATEs with limited capacities. In this paper, we present a novel approach to this challenge by run-time coordinating the algorithm and ATE. A unique combination of a #SAT solver, checksum computation and frame testing enables the efficient incremental testing. Unlike checksums from the communication domain which can only detect the existence of stuck-at faults, our approach differentiates by also locating them. In our experimental results, our method further demonstrates a shorter testing time.

Testing constraints for real-time systems are usually verified through the satisfiability of propositional formulae. In this paper, we propose an alternative where the verification of timing constraints can be done by counting the number of truth assignments instead of Boolean satisfiability. This number can also tell us how "far away" a given specification is from satisfying its safety assertion. Furthermore, specifications and safety assertions are often modified in an incremental fashion, where problematic bugs are fixed one at a time. To support this development, we propose an incremental algorithm for counting satisfiability. Our proposed incremental algorithm is optimal as no unnecessary nodes are created during each counting. This works for the class of expressions, known as path RTL ([F. Jahanian et al. (1987), F. Wang et al. (1994)]). To illustrate this application, we show how incremental satisfiability counting can be applied to a well-known rail-road crossing example, particularly when its specification is still being refined.