Misplaced Pages

#800199

55-599: Lunar IceCube is a NASA nanosatellite orbiter mission that was intended to prospect, locate, and estimate amount and composition of water ice deposits on the Moon for future exploitation. It was launched as a secondary payload mission on Artemis 1 (formerly known as Exploration Mission 1), the first flight of the Space Launch System (SLS), on 16 November 2022. As of February 2023 it is unknown whether NASA team has contact with satellite or not. The lunar mission

110-435: A formation . The generic term "small satellite" or "smallsat" is also sometimes used, as is "satlet". Examples: Astrid-1 and Astrid-2, as well as the set of satellites currently announced for LauncherOne (below) In 2018, the two Mars Cube One microsats—massing just 13.5 kg (30 lb) each—became the first CubeSats to leave Earth orbit for use in interplanetary space. They flew on their way to Mars alongside

165-464: A 10 kg (22 lb) payload into a 250 km (160 mi) orbit to an even-more-capable clustered "20/450 Nano/Micro Satellite Launch Vehicle" (NMSLV) capable of delivering 20 kg (44 lb) payloads into 450 km (280 mi) circular orbits . The Boeing Small Launch Vehicle is an air-launched three-stage-to-orbit launch vehicle concept aimed to launch small payloads of 45 kg (100 lb) into low Earth orbit. The program

220-547: A given subprogram. At a minimum, the GNATprove will generate VCs to establish that all run-time errors cannot occur within a subprogram, such as: If a postcondition or any other assertion is added to a subprogram, GNATprove will also generate VCs that require the user to show that these properties hold for all possible paths through the subprogram. Under the hood, GNATprove uses the Why3 intermediate language and VC Generator, and

275-435: A larger "mother" satellite for communication with ground controllers or for launching and docking with picosatellites. Picosatellites are emerging as a new alternative for do-it-yourself kitbuilders. Picosatellites are currently commercially available across the full range of 0.1–1 kg (0.22–2.2 lb). Launch opportunities are now available for $ 12,000 to $ 18,000 for sub-1 kg picosat payloads that are approximately

330-425: A market value estimated at US$ 7.4 billion . By mid-2015, many more launch options had become available for smallsats, and rides as secondary payloads had become both greater in quantity and easier to schedule on shorter notice. In a surprising turn of events, the U.S. Department of Defense , which had for decades procured heavy satellites on decade-long procurement cycles, is making a transition to smallsats in

385-515: A mass of about 14 kg (31 lb). It is one of ten CubeSats carried on board the maiden flight of the SLS, Artemis 1 , as secondary payloads in cis-lunar space, in 2022. It was deployed during the lunar trajectory, and was intended to use an innovative electric RF ion engine to achieve lunar capture to an orbit about 100 km (62 mi) above the lunar surface, to make systematic measurements of lunar water features. The principal investigator

440-433: A mass of no more than 1.33 kilograms (2.9 lb) per unit. The CubeSat concept was first developed in 1999 by a collaborative team of California Polytechnic State University and Stanford University , and the specifications, for use by anyone planning to launch a CubeSat-style nanosatellite, are maintained by this group. With continued advances in the miniaturization and capability increase of electronic technology and

495-474: A number of companies began development of launch vehicles specifically targeted at the smallsat market. In particular, with larger numbers of smallsats flying, the secondary payload paradigm does not provide the specificity required for many small satellites that have unique orbital and launch-timing requirements. Some USA-based private companies that at some point in time have launched smallsat launch vehicles commercially: The term "microsatellite" or "microsat"

550-555: Is Ben Malphrus, Director of the Space Science Center at Morehead State University . NASA's Lunar Prospector , Clementine , Lunar Crater Observation and Sensing Satellite ( LCROSS ), the Lunar Reconnaissance Orbiter (LRO) and India's Chandrayaan-1 lunar orbiters and other missions, confirmed both water (H 2 O) and hydroxyl (—OH) deposits at high latitudes on the lunar surface, indicating

605-599: Is a formally defined computer programming language based on the Ada programming language, intended for the development of high integrity software used in systems where predictable and highly reliable operation is essential. It facilitates the development of applications that demand safety, security, or business integrity. Originally, there were three versions of the SPARK language (SPARK83, SPARK95, SPARK2005) based on Ada 83, Ada 95 and Ada 2005 respectively. A fourth version of

SECTION 10

#1732790900801

660-681: Is designed to form a quantum communication network as well as communicate with Earth through an optical ground station. The term "small satellite", or sometimes "minisatellite", often refers to an artificial satellite with a wet mass (including fuel) between 100 and 500 kg (220 and 1,100 lb), but in other usage has come to mean any satellite under 500 kg (1,100 lb). Small satellite examples include Demeter , Essaim , Parasol , Picard , MICROSCOPE , TARANIS , ELISA , SSOT , SMART-1 , Spirale-A and -B , and Starlink satellites. Although smallsats have traditionally been launched as secondary payloads on larger launch vehicles,

715-568: Is estimated the spacecraft will take about 3 months to reach the Moon. The flight software was developed in SPARK/Ada by the Vermont Technical College Cubesat Laboratory . SPARK/Ada has the lowest error rate of any computer language, important for the reliability and success of this complicated spacecraft. It is used in commercial and military aircraft, air traffic control and high speed trains. This

770-517: Is proposed to drive down launch costs for U.S. military small satellites to as low as US$ 300,000 per launch ($ 7,000/kg) and, if the development program was funded, as of 2012 could be operational by 2020. The Swiss company Swiss Space Systems (S3) has announced plans in 2013 to develop a suborbital spaceplane named SOAR that would launch a microsat launch vehicle capable of putting a payload of up to 250 kg (550 lb) into low Earth orbit. The Spanish company PLD Space born in 2011 with

825-695: Is the opportunity to enable missions that a larger satellite could not accomplish, such as: The nanosatellite and microsatellite segments of the satellite launch industry have been growing rapidly in the 2010s. Development activity in the 1–50 kg (2.2–110.2 lb) range has been significantly exceeding that in the 50–100 kg (110–220 lb) range. In the 1–50 kg range alone, fewer than 15 satellites were launched annually in 2000 to 2005, 34 in 2006, then fewer than 30 launches annually during 2007 to 2011. This rose to 34 launched in 2012 and 92 launched in 2013. European analyst Euroconsult projects more than 500 smallsats being launched in 2015–2019 with

880-1076: Is the second spacecraft using SPARK/Ada, the first being the BasicLEO CubeSat also by the Vermont Technical College CubeSat Laboratory, the only fully successful university CubeSat out of 12 on the NASA ELaNa-IV launch on U.S. Air Force Operationally Responsive Space-3 (ORS-3) mission. Nanosatellite One rationale for miniaturizing satellites is to reduce the cost; heavier satellites require larger rockets with greater thrust that also have greater cost to finance. In contrast, smaller and lighter satellites require smaller and cheaper launch vehicles and can sometimes be launched in multiples. They can also be launched 'piggyback', using excess capacity on larger launch vehicles. Miniaturized satellites allow for cheaper designs and ease of mass production. Another major reason for developing small satellites

935-422: Is usually applied to the name of an artificial satellite with a wet mass between 10 and 100 kg (22 and 220 lb). However, this is not an official convention and sometimes those terms can refer to satellites larger than that, or smaller than that (e.g., 1–50 kg (2.2–110.2 lb)). Sometimes, designs or proposed designs from some satellites of these types have microsatellites working together or in

990-556: The New Horizons Pluto flyby mission. The tiny CubeSat spacecraft will make use of a miniature electric RF ion engine system based on Busek 's 3 centimeter RF ion thruster, also known as BIT-3 . It utilizes a solid iodine propellant and an inductively-coupled plasma system that produces 1.1 mN thrust and 2800 seconds specific impulse from approximately 50 watts total input power. It will also use this engine for capture into lunar orbit, and orbit adjustments. It

1045-544: The CVC4 , Z3 , and Alt-Ergo theorem provers to discharge VCs. Use of other provers (including interactive proof checkers) is also possible through other components of the Why3 toolset. The first version of SPARK (based on Ada 83) was produced at the University of Southampton (with UK Ministry of Defence sponsorship) by Bernard Carré and Trevor Jennings. The name SPARK was derived from SPADE Ada Kernel , in reference to

1100-486: The PicoSAT series of microsatellites) is usually applied to artificial satellites with a wet mass between 0.1 and 1 kg (0.22 and 2.2 lb), although it is sometimes used to refer to any satellite that is under 1 kg in launch mass. Again, designs and proposed designs of these types usually have multiple picosatellites working together or in formation (sometimes the term "swarm" is applied). Some designs require

1155-552: The SPADE subset of the Pascal programming language . Subsequently the language was progressively extended and refined, first by Program Validation Limited and then by Praxis Critical Systems Limited. In 2004, Praxis Critical Systems Limited changed its name to Praxis High Integrity Systems Limited. In January 2010, the company became Altran Praxis . In early 2009, Praxis formed a partnership with AdaCore, and released "SPARK Pro" under

SECTION 20

#1732790900801

1210-606: The 2020s. The office of space acquisition and integration said in January 2023 that "the era of massive satellites needs to be in the rear view mirror for the Department of Defense" with small satellites being procured for DoD needs in all orbital regimes, regardless of "whether it's LEO MEO or GEO " while aiming for procurements in under three years. The smaller satellites are deemed to be harder for an enemy to target, as well as providing more resilience through redundancy in

1265-478: The CubeSat so that it can be placed into its science orbit in the coming days.” The site has not been updated since, and the status of the spacecraft is unknown. Lunar IceCube carried a Broadband InfraRed Compact High Resolution Exploration Spectrometer (BIRCHES) instrument, developed by NASA's Goddard Space Flight Center (GSFC). BIRCHES is a compact version of the volatile-seeking spectrometer instrument onboard

1320-528: The DARPA SeeMe program that intended to release a " constellation of 24 micro-satellites (~20 kg (44 lb) range) each with 1-m imaging resolution ." The program was cancelled in December 2015. In April 2013, Garvey Spacecraft was awarded a US$ 200,000 contract to evolve their Prospector 18 suborbital launch vehicle technology into an orbital nanosat launch vehicle capable of delivering

1375-513: The GNAT Ada 2012 front-end. SPARK utilises the strengths of Ada while trying to eliminate all its potential ambiguities and insecure constructs. SPARK programs are by design meant to be unambiguous, and their behavior is required to be unaffected by the choice of Ada compiler . These goals are achieved partly by omitting some of Ada's more problematic features (such as unrestricted parallel tasking ) and partly by introducing contracts which encode

1430-457: The ISS external platform Materials International Space Station Experiment (MISSE-8) for testing. In April 2014, the nanosatellite KickSat was launched aboard a Falcon 9 rocket with the intention of releasing 104 femtosatellite-sized chipsats, or "Sprites". In the event, they were unable to complete the deployment on time due to a failure of an onboard clock and the deployment mechanism reentered

1485-451: The SPARK language, SPARK 2014, based on Ada 2012, was released on April 30, 2014. SPARK 2014 is a complete re-design of the language and supporting verification tools. The SPARK language consists of a well-defined subset of the Ada language that uses contracts to describe the specification of components in a form that is suitable for both static and dynamic verification. In SPARK83/95/2005,

1540-527: The SPARK version run only about 5 to 10% slower than C. Later improvement to the Ada middle-end in GCC (implemented by Eric Botcazou of AdaCore) closed the gap, with the SPARK code matching the C in performance exactly. NVIDIA have also adopted SPARK for the implementation of security-critical firmware. In 2020, Rod Chapman re-implemented the TweetNaCl cryptographic library in SPARK 2014. The SPARK version of

1595-508: The application designer's intentions and requirements for certain components of a program. The combination of these approaches allows SPARK to meet its design objectives, which are: Consider the Ada subprogram specification below: In pure Ada this might increment the variable X by one or one thousand; or it might set some global counter to X and return the original value of the counter in X ; or it might do absolutely nothing with X at all. With SPARK 2014, contracts are added to

1650-927: The atmosphere and burned up. Small satellites usually require innovative propulsion, attitude control , communication and computation systems. Larger satellites usually use monopropellants or bipropellant combustion systems for propulsion and attitude control; these systems are complex and require a minimal amount of volume to surface area to dissipate heat. These systems may be used on larger small satellites, while other micro/nanosats have to use electric propulsion, compressed gas, vaporizable liquids such as butane or carbon dioxide or other innovative propulsion systems that are simple, cheap and scalable. Small satellites can use conventional radio systems in UHF, VHF, S-band and X-band, although often miniaturized using more up-to-date technology as compared to larger satellites. Tiny satellites such as nanosats and small microsats may lack

1705-608: The atmosphere on 14 May 2014, without having deployed any of the 5-gram femtosats. ThumbSat is another project intending to launch femtosatellites in the late 2010s. ThumbSat announced a launch agreement with CubeCat in 2017 to launch up to 1000 of the very small satellites. In March 2019, the CubeSat KickSat-2 deployed 105 femtosats called "ChipSats" into Earth orbit. Each of the ChipSats weighed 4 grams. The satellites were tested for 3 days, and they then reentered

Lunar IceCube - Misplaced Pages Continue

1760-484: The code to provide additional information regarding what a subprogram actually does. For example, we may alter the above specification to say: This specifies that the Increment procedure does not use (neither update nor read) any global variable and that the only data item used in calculating the new value of X is X itself. Alternatively, the designer might specify: This specifies that Increment will use

1815-467: The contracts are encoded in Ada comments and so are ignored by any standard Ada compiler, but are processed by the SPARK "Examiner" and its associated tools. SPARK 2014, in contrast, uses Ada 2012's built-in "aspect" syntax to express contracts, bringing them into the core of the language. The main tool for SPARK 2014 (GNATprove) is based on the GNAT/GCC infrastructure , and re-uses almost the entirety of

1870-683: The design of LauncherOne". Virgin Orbit has been working on the LauncherOne concept since late 2008, and as of 2015 , is making it a larger part of Virgin's core business plan as the Virgin human spaceflight program has experienced multiple delays and a fatal accident in 2014. In December 2012, DARPA announced that the Airborne Launch Assist Space Access program would provide the microsatellite rocket booster for

1925-670: The design of a large distributed network of satellite assets . In 2021, the first autonomous nanosatellites , part of the Adelis-SAMSON mission, designed and developed by the Technion and Rafael in Israel were launched into space. In 2023, SpaceX launched a 20cm quantum communication nano satellite developed by the Tel Aviv University , it is the world's first quantum communication satellite. TAU's nanosatellite

1980-535: The development of the original MULTOS CA, the NSA Tokeneer demonstrator, the secunet multi-level workstation, the Muen separation kernel and Genode block-device encrypter. In August 2010, Rod Chapman, principal engineer of Altran Praxis, implemented Skein , one of candidates for SHA-3 , in SPARK. In comparing the performance of the SPARK and C implementations and after careful optimization, he managed to have

2035-428: The emergence of the technological advances of miniaturization and increased capital to support private spaceflight initiatives in the 2010s, several startups have been formed to pursue opportunities with developing a variety of small-payload Nanosatellite Launch Vehicle (NLV) technologies. NLVs proposed or under development include: Actual NS launches: The term "picosatellite" or "picosat" (not to be confused with

2090-479: The following: This, now, specifies not only that X is derived from itself alone, but also that before Increment is called X must be strictly less than the last possible value of its type (to ensure that the result will never overflow ) and that afterwards X will be equal to the initial value of X plus one. GNATprove can also generate a set of verification conditions or VCs. These conditions are used to establish whether certain properties hold for

2145-400: The global variable Count in the same package as Increment , that the exported value of Count depends on the imported values of Count and X , and that the exported value of X does not depend on any variables at all and it will be derived from constant data only. If GNATprove is then run on the specification and corresponding body of a subprogram, it will analyse the body of

2200-482: The objective of developing low cost launch vehicles called Miura 1 and Miura 5 with the capacity to place up to 150 kg (330 lb) into orbit. The term "nanosatellite" or "nanosat" is applied to an artificial satellite with a wet mass between 1 and 10 kg (2.2 and 22.0 lb). Designs and proposed designs of these types may be launched individually, or they may have multiple nanosatellites working together or in formation, in which case, sometimes

2255-672: The opportunity to test new hardware with reduced expense in testing. Furthermore, since the overall cost risk in the mission is much lower, more up-to-date but less space-proven technology can be incorporated into micro and nanosats than can be used in much larger, more expensive missions with less appetite for risk. Small satellites are difficult to track with ground-based radar, so it is difficult to predict if they will collide with other satellites or human-occupied spacecraft. The U.S. Federal Communications Commission has rejected at least one small satellite launch request on these safety grounds. SPARK (programming language) SPARK

Lunar IceCube - Misplaced Pages Continue

2310-514: The power supply or mass for large conventional radio transponders , and various miniaturized or innovative communications systems have been proposed, such as laser receivers, antenna arrays and satellite-to-satellite communication networks. Few of these have been demonstrated in practice. Electronics need to be rigorously tested and modified to be "space hardened" or resistant to the outer space environment (vacuum, microgravity, thermal extremes, and radiation exposure). Miniaturized satellites allow for

2365-416: The presence of trace amounts of adsorbed or bound water are present, but their instruments weren't optimized for fully or systematically characterizing the elements in the infrared wavelength bands ideal for detecting water. These missions suggest that there might be enough ice water at polar regions to be used by future landed missions, but the distribution is difficult to reconcile with thermal maps. Thus,

2420-934: The same mission cost, with significantly increased revisit times: every area of the globe can be imaged every 3.5 hours rather than the once per 24 hours with the RapidEye constellation. More rapid revisit times are a significant improvement for nations performing disaster response, which was the purpose of the RapidEye constellation. Additionally, the nanosat option would allow more nations to own their own satellite for off-peak (non-disaster) imaging data collection. As costs lower and production times shorten, nanosatellites are becoming increasingly feasible ventures for companies. Example nanosatellites: ExoCube (CP-10) , ArduSat , SPROUT Nanosatellite developers and manufacturers include EnduroSat , GomSpace , NanoAvionics , NanoSpace, Spire , Surrey Satellite Technology , NovaWurks , Dauria Aerospace , Planet Labs and Reaktor . In

2475-447: The science goals were to investigate the distribution of water and other volatiles , as a function of time of day, latitude , and lunar soil composition. The cubesat was launched on November 16, 2022 on the Space Launch System "Artemis 1" launch. The vehicle successfully communicated with the ground after deployment on Nov. 17, but on Nov. 29 2022, NASA announced that the mission team was “continuing its attempts to communicate with

2530-690: The secondary payload paradigm does not provide the specificity required for many increasingly sophisticated small satellites that have unique orbital and launch-timing requirements. In July 2012, Virgin Orbit announced LauncherOne , an orbital launch vehicle designed to launch "smallsat" primary payloads of 100 kg (220 lb) into low Earth orbit , with launches projected to begin in 2016. Several commercial customers have already contracted for launches, including GeoOptics , Skybox Imaging , Spaceflight Industries , and Planetary Resources . Both Surrey Satellite Technology and Sierra Nevada Space Systems are developing satellite buses "optimized to

2585-531: The size of a soda can. The term "femtosatellite" or "femtosat" is usually applied to artificial satellites with a wet mass below 100 g (3.5 oz). Like picosatellites, some designs require a larger "mother" satellite for communication with ground controllers. Three prototype "chip satellites" were launched to the ISS on Space Shuttle Endeavour on its final mission in May 2011. They were attached to

2640-453: The subprogram to build up a model of the information flow. This model is then compared against that which has been specified by the annotations and any discrepancies reported to the user. These specifications can be further extended by asserting various properties that either need to hold when a subprogram is called ( preconditions ) or that will hold once execution of the subprogram has completed ( postconditions ). For example, we could say

2695-613: The successful Mars InSight lander mission. The two microsats accomplished a flyby of Mars in November 2018, and both continued communicating with ground stations on Earth through late December. Both went silent by early January 2019. A number of commercial and military-contractor companies are currently developing microsatellite launch vehicles to perform the increasingly targeted launch requirements of microsatellites. While microsatellites have been carried to space for many years as secondary payloads aboard larger launchers ,

2750-564: The ten years of nanosat launches prior to 2014, only 75 nanosats were launched. Launch rates picked up substantially when in the three-month period from November 2013–January 2014 94 nanosats were launched. One challenge of using nanosats has been the economic delivery of such small satellites to anywhere beyond low Earth orbit . By late 2014, proposals were being developed for larger spacecraft specifically designed to deliver swarms of nanosats to trajectories that are beyond Earth orbit for applications such as exploring distant asteroids. With

2805-417: The term "satellite swarm" or " fractionated spacecraft " may be applied. Some designs require a larger "mother" satellite for communication with ground controllers or for launching and docking with nanosatellites. Over 2300 nanosatellites have been launched as of December 2023. A CubeSat is a common type of nanosatellite, built in cube form based on multiples of 10 cm × 10 cm × 10 cm, with

SECTION 50

#1732790900801

2860-767: The terms of the GPL. This was followed in June 2009 by the SPARK GPL Edition 2009, aimed at the FOSS and academic communities. In June 2010, Altran-Praxis announced that the SPARK programming language would be used in the software of US Lunar project CubeSat , expected to be completed in 2015. In January 2013, Altran-Praxis changed its name to Altran which in April 2021 became Capgemini Engineering (following Altran's merger with Capgemini ). The first Pro release of SPARK 2014

2915-414: The use of satellite constellations , nanosatellites are increasingly capable of performing commercial missions that previously required microsatellites. For example, a 6U CubeSat standard has been proposed to enable a satellite constellation of thirty five 8 kg (18 lb) Earth-imaging satellites to replace a constellation of five 156 kg (344 lb) RapidEye Earth-imaging satellites, at

2970-1093: Was announced on April 30, 2014, and was quickly followed by the SPARK 2014 GPL edition, aimed at the FLOSS and academic communities. SPARK has been used in several high profile safety-critical systems, covering commercial aviation ( Rolls-Royce Trent series jet engines, the ARINC ACAMS system , the Lockheed Martin C130J ), military aviation ( EuroFighter Typhoon , Harrier GR9 , AerMacchi M346 ), air-traffic management (UK NATS iFACTS system), rail (numerous signalling applications), medical (the LifeFlow ventricular assist device ), and space applications (the Vermont Technical College CubeSat project ). SPARK has also been used in secure systems development. Users include Rockwell Collins (Turnstile and SecureOne cross-domain solutions),

3025-487: Was designed by Morehead State University and its partners, the Busek Company , NASA Goddard Space Flight Center (GSFC), and The Catholic University of America (CUA). It was selected in April 2015 by NASA's NextSTEP program ( Next Space Technologies for Exploration Partnerships ) and awarded a contract worth up to US$ 7.9 million for further development. The Lunar IceCube spacecraft has a 6U CubeSat format, with

#800199